Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Deciding unique inhabitants with sums (work in progress)

Abstract : Our ongoing work focuses on types that have a unique inhabitant—modulo program equivalence. If we were able to detect when such types appear in a program, we could perform program inference to releave the programmer from the obligation to write the less-interesting parts of the program. Unicity of inhabitant is a strong form of principality: inference cannot make a "wrong" guess as there is only one choice. To decide uniqueness, we must be able to enumerate the distinct terms at a given type. As a first step, we consider the simply-typed lambda-calculus with arrows, product and sums. We are looking for a term enumeration process that is complete, i.e., it does not miss any computational behavior, and canonical, i.e., it has no duplicates. We propose an approach based on saturation, with encouraging results, although termination is still a conjecture.
Document type :
Conference papers
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download
Contributor : Scherer Gabriel Connect in order to contact the contributor
Submitted on : Thursday, December 18, 2014 - 9:08:10 AM
Last modification on : Thursday, February 3, 2022 - 11:14:57 AM
Long-term archiving on: : Saturday, April 15, 2017 - 7:56:14 AM


Files produced by the author(s)

Résumé du travail soumis à la relecture


  • HAL Id : hal-01094127, version 1



Gabriel Scherer, Didier Rémy. Deciding unique inhabitants with sums (work in progress). TYPES, May 2014, Paris, France. ⟨hal-01094127⟩



Record views


Files downloads