A simple proof of the undecidability of inhabitation in λP

DOI10.1017/S0956796800001969zbMath0872.68035MaRDI QIDQ3125231

Marc Bezem, Jan Springintveld

Publication date: 18 March 1997

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

inhabitation problem

Mathematics Subject Classification ID

Related Items (3)

Realist Consequence, Epistemic Inference, Computational Correctness ⋮ Introduction to Type Theory ⋮ Proof-term synthesis on dependent-type systems via explicit substitutions

Cites Work

• Embedding first order predicate logic in fragments of intuitionistic logic
• Computability of Recursive Functions

This page was built for publication: A simple proof of the undecidability of inhabitation in λP