16 citations · 18 across the 6 of their papers we have counts for
6 papers
A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version)
Pedro H. Azevedo de Amorim, Mayuko Kori, Koko Muroya
In this paper we present a framework for modelling \emph{reward-sensitive bisimulations}, that is, bisimulations that account for quantitative differences such as accumulated rewar…
Logical relations for call-by-push-value models, via internal fibrations in a 2-category
Pedro H. Azevedo de Amorim, Satoshi Kura, Philip Saville
We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise…
Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus (Extended Version)
Steven Schaefer, Nathan Varner, Pedro H. Azevedo de Amorim +1
We present Dependent Lambek Calculus, a domain-specific dependent type theory for verified parsing and formal grammar theory. In , linear types are used as a syn…
Modular Hardware Design with Timeline Types
Rachit Nigam, Pedro Henrique Azevedo De Amorim, Adrian Sampson
Modular design is a key challenge for enabling large-scale reuse of hardware modules. Unlike software, however, hardware designs correspond to physical circuits and inherit constra…
Universal Semantics for the Stochastic Lambda-Calculus
Pedro Amorim, Dexter Kozen, Radu Mardare +2
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techn…
First-Order Logic for Flow-Limited Authorization
Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti +2
We present the Flow-Limited Authorization First-Order Logic (FLAFOL), a logic for reasoning about authorization decisions in the presence of information-flow policies. We formalize…