Pedro Henrique
Azevedo de Amorim

I am a fourth-year PhD candidate 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.

I co-organize Cornell's Programming Language Discussion Group

Office: 456 Gates Hall

April 2021 Our paper Universal Semantics for the Stochastic Lambda-Calculus has been selected to appear at LICS 2021!

November 2020 Our preprint Universal Semantics for the Stochastic Lambda-Calculus is now on the arXiv.

December 2019 Our paper First-Order Logic for Flow-Limited Authorization was selected to appear at CSF 2020!

June 2019 I attended OPLSS.

August 2018 I started my PhD at Cornell!


Preprints and Drafts

Linear Polymorphism and Naturality. Pedro H. Azevedo de Amorim, Dexter Kozen and Michael Roberts

Distribution Theoretic Semantics for Non-Smooth Differentiable Programming. Pedro H. Azevedo de Amorim and Christopher Lam

Classical and Differential Linear Logic in Riesz Spaces: Semantical Foundations for Differentiable Probabilistic Programming. Pedro H. Azevedo de Amorim and Dexter Kozen

Refereed Publications

Universal Semantics for the Stochastic Lambda-Calculus. Pedro H. Azevedo de Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden, Michael Roberts
To appear at LICS 2021 (online) [Preprint]

First-Order Logic for Flow-Limited Authorization. Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, Owen Arden.
CSF 2020, Boston, USA [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]

Spring 2020 Teaching Assistant for CS3110 : Data Structures and Functional Programming

Fall 2019 Teaching Assistant for CS4810 : Introduction to Theory of Computation

Spring 2019 Teaching Assistant for CS4120 : Introduction to Compilers

Fall 2018 Teaching Assistant for CS4110 : Programming Languages and Logics