Pedro Henrique Azevedo de Amorim

I am a Research Associate at the department of Computer Science of the University of Oxford where I work with Sam Staton. Prior to that I completed my PhD at the Computer Science Department at Cornell University working with Dexter Kozen.

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 applications of substructural logics to programming languages.

Office: 309 Wolfson Building
Email:

News

April 2025 Our paper Logical relations for call-by-push-value models, via internal fibrations in a 2-category has been selected to appear at LICS 2025!

April 2025 Our paper Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus has been selected to appear at PLDI 2025!

Feb 2025 My paper Denotational Foundations for Expected Cost Analysis has been selected to appear at OOPSLA 2025!

Oct 2024 Our paper Classical Linear Logic in Perfect Banach Spaces has been selected to appear at CSL 2025!

Jan 2024 My preprint on semantics for expected cost of functional programs is out

Sep 2023 I have moved to Oxford!

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]

Conferences

Denotational Foundations for Expected Cost Analysis.
Pedro H. Azevedo de Amorim
OOPSLA 2025 (to appear) [Preprint] [DOI]

Logical relations for call-by-push-value models, via internal fibrations in a 2-category.
Pedro H. Azevedo de Amorim, Satoshi Kura, Philip Saville
LICS 2025 (to appear) [Preprint]

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus.
Steven Schaefer, Nathan Varner, Pedro H. Azevedo de Amorim and Max S. New
PLDI 2025 (to appear) [Extended version]

Classical Linear Logic in Perfect Banach Lattices.
Pedro H. Azevedo de Amorim, Leon Witzman and Dexter Kozen
CSL 2025, Amsterdam, Netherlands [Preprint] [DOI]

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

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

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] [DOI]

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 [Extended version] [DOI]

A Specification for Dependently-Typed Haskell.
Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg.
ICFP 2017, Oxford, UK [DOI]