Pedro Henrique Azevedo de Amorim

I have finished my PhD at the Computer Science Department at Cornell University where I was advised by 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 probabilistic programming languages and differentiable programming languages.

Office: 456 Gates Hall
Email:

News

Jul 2023 I have finished my PhD!

Dec 2022 My paper A Higher-Order Language for Markov Kernels and Linear Operators has been selected to appear at FoSSaCS 2023!

Jul 2022 Our preprint A Distribution-Theoretic Semantics for Non-Smooth Differentiable Programming is now on the arXiv.

Feb 2022 My preprint A Sampling-Aware interpretation of Linear Logic: Syntax and Categorical Semantics is now on the arXiv.

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

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

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

Jun 2019 I attended OPLSS.

Aug 2018 I started my PhD at Cornell!

Publications

Preprints and Drafts

Separated and Shared Effects in Higher-Order Languages Pedro H. Azevedo de Amorim and Justin Hsu [Preprint]

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

Classical Linear Logic in Perfect Banach Lattices. Pedro H. Azevedo de Amorim, Leon Witzman and Dexter Kozen

Conferences

Modular Hardware Design with Timeline Types. Rachit Nigam, Pedro H. Azevedo de Amorim and Adrian Sampson
PLDI 2023, Orlando, USA

A Higher-Order Language for Markov Kernels and Linear Operators. Pedro H. Azevedo de Amorim
FoSSaCS 2023, Paris, France [Preprint]

Universal Semantics for the Stochastic Lambda-Calculus. Pedro H. Azevedo de Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden and Michael Roberts
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]