@inproceedings{6c84a42bf861420f85c483137bf78b21,
title = "Which simple types have a unique inhabitant?",
abstract = "We study the question of whether a given type has a unique inhabitant modulo program equivalence. In the setting of simplytyped lambda-calculus with sums, equipped with the strong βη-equivalence, we show that uniqueness is decidable. We present a saturating focused logic that introduces irreducible cuts on positive types {"}as soon as possible{"}. Backward search in this logic gives an effective algorithm that returns either zero, one or two distinct inhabitants for any given type. Preliminary application studies show that such a feature can be useful in strongly-typed programs, inferring the code of highly-polymorphic library functions, or {"}glue code{"} inside more complex terms.",
keywords = "Calculus, Canonicity, Code inference, Focusing, Proof search, Saturation, Simply, Sums, Typed lambda, Unique inhabitants",
author = "Gabriel Scherer and Didier R{\'e}my",
year = "2015",
month = aug,
day = "29",
doi = "10.1145/2784731.2784757",
language = "English",
series = "Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP",
publisher = "Association for Computing Machinery",
pages = "243--255",
editor = "Kathleen Fisher and John Reppy",
booktitle = "ICFP 2015 - Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming",
note = "20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015 ; Conference date: 31-08-2015 Through 02-09-2015",
}