Which simple types have a unique inhabitant?

DOI10.1145/2784731.2784757zbMath1360.68341OpenAlexW2000862401MaRDI QIDQ2981966

Didier Rémy, Gabriel Scherer

Publication date: 10 May 2017

Published in: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2784731.2784757

zbMATH Keywords

saturationfocusingproof searchsumscanonicitysimply-typed lambda-calculuscode inferenceunique inhabitants

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Maximally multi-focused proofs for skew non-commutative \texttt{MILL}

This page was built for publication: Which simple types have a unique inhabitant?