16 citations · 18 across the 6 of their papers we have counts for
Showing 2025Show all
2 papers · 1 filter
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…