3 papers
cs.LO2026
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…
cs.LO2025
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…
cs.PL2025
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…