Pedro Henrique
Azevedo de Amorim

I am a first-year PhD student at the Computer Science Department at Cornell University working with Dexter Kozen. Prior to that I was a research intern at MIT and UPenn where I worked, respectively, with Adam Chlipala and Stephanie Weirich

My research interests lie mainly in formal verification, programming language theory, and their intersection. In particular I'm interested in applications of Category Theory, Type Theory, Proof Assistants and Logic to programming languages.

Recently I've been interested in the semantics of higher-order probabilistic programming languages.


Office: 350 Gates Hall
Email:
News

June 2019 I attended OPLSS

August 2018 I started my PhD at Cornell!

Publications

First-Order Logic for Flow-Limited Authorization. Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, Owen Arden. [Tech Report]
A Specification for Dependently-Typed Haskell. Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg. ICFP 2017, Oxford, UK [Paper]
Teaching

Spring 2019 Teaching Assistant for CS4120 : Introduction to Compilers

Fall 2018 Teaching Assistant for CS4110 : Programming Languages and Logics