Why Are Proofs Relevant in Proof-Relevant Models?*

Kerinec, A; Manzonetto, G; Olimpieri, F

Kerinec, A (通讯作者),Univ Sorbonne Paris Nord, LIPN, CNRS UMR 7030, Paris, France.

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023; 7 (POPL):

Abstract

Relational models of lambda-calculus can be presented as type systems, the relational interpretation of a lambda-term being given by the set of its ty......

Full Text Link