A specification for dependent types in Haskell. - Stephanie Weirich; Antoine Voizard; Pedro Henrique Azevedo de Amorim; Richard A. Eisenberg (Proc. ACM Program. Lang., 2017)

First-Order Logic for Flow-Limited Authorization. - Andrew K. Hirsch; Pedro H. Azevedo de Amorim; Ethan Cecchetti; Ross Tate; Owen Arden (CSF, 2020)

Universal Semantics for the Stochastic Lambda-Calculus. - Pedro H. Azevedo de Amorim; Dexter Kozen; Radu Mardare; Prakash Panangaden; Michael Roberts (CoRR, 2020)

Universal Semantics for the Stochastic λ-Calculus. - Pedro H. Azevedo de Amorim; Dexter Kozen; Radu Mardare; Prakash Panangaden; Michael Roberts (LICS, 2021)

A Sampling-Aware Interpretation of Linear Logic: Syntax and Categorical Semantics. - Pedro H. Azevedo de Amorim (CoRR, 2022)

Distribution Theoretic Semantics for Non-Smooth Differentiable Programming. - Pedro H. Azevedo de Amorim; Christopher Lam 003 (CoRR, 2022)

A Higher-Order Language for Markov Kernels and Linear Operators. - Pedro H. Azevedo de Amorim (FoSSaCS, 2023)

Separated and Shared Effects in Higher-Order Languages. - Pedro H. Azevedo de Amorim; Justin Hsu (CoRR, 2023)

Modular Hardware Design with Timeline Types. - Rachit Nigam; Pedro Henrique Azevedo de Amorim; Adrian Sampson (Proc. ACM Program. Lang., 2023)

Compositional Expected Cost Analysis of Functional Probabilistic Programs. - Pedro H. Azevedo de Amorim (CoRR, 2024)

Classical Linear Logic in Perfect Banach Lattices. - Pedro H. Azevedo de Amorim; Leon Witzman; Dexter Kozen (CSL, 2025)

Denotational Foundations for Expected Cost Analysis. - Pedro H. Azevedo de Amorim (Proc. ACM Program. Lang., 2025)

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus. - Steven Schaefer; Nathan Varner; Pedro Henrique Azevedo de Amorim; Max S. New (Proc. ACM Program. Lang., 2025)

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus (Extended Version). - Steven Schaefer; Nathan Varner; Pedro H. Azevedo de Amorim; Max S. New (CoRR, 2025)

Logical relations for call-by-push-value models, via internal fibrations in a 2-category. - Pedro H. Azevedo de Amorim; Satoshi Kura 003; Philip Saville (CoRR, 2025)