Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

DOI10.2168/LMCS-2(2:1)2006zbMath1126.03019arXivmath/0602544MaRDI QIDQ5310654

Kristian Støvring

Publication date: 11 October 2007

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/math/0602544

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (7)

Unnamed Item ⋮ Cartesian Monoids ⋮ Extensional proofs in a propositional logic modulo isomorphisms ⋮ On polymorphic types of untyped terms ⋮ How to think of intersection types as Cartesian products ⋮ Functional pearl: the distributive \(\lambda\)-calculus ⋮ Unnamed Item

Uses Software

• Twelf

This page was built for publication: Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative