A Unifying Framework for Type Inhabitation

Authors Sandra Alves , Sabine Broda

Thumbnail PDF


  • Filesize: 489 kB
  • 16 pages

Document Identifiers

Author Details

Sandra Alves
  • DCC-Faculty of Science & CRACS, University of Porto, Portugal
Sabine Broda
  • DCC-Faculty of Science & CMUP, University of Porto, Portugal

Cite AsGet BibTex

Sandra Alves and Sabine Broda. A Unifying Framework for Type Inhabitation. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


In this paper we define a framework to address different kinds of problems related to type inhabitation, such as type checking, the emptiness problem, generation of inhabitants and counting, in a uniform way. Our framework uses an alternative representation for types, called the pre-grammar of the type, on which different methods for these problems are based. Furthermore, we define a scheme for a decision algorithm that, for particular instantiations of the parameters, can be used to show different inhabitation related problems to be in PSPACE.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Lambda calculus
  • Theory of computation → Rewrite systems
  • simple types
  • type inhabitation
  • rewriting


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Sandra Alves and Sabine Broda. Inhabitation machines: determinism and principality. In %Ninth Workshop on Non-Classical Models of Automata and Applications, NCMA 2017, pages 57-70, 2017. Google Scholar
  2. Ch. Ben-Yelles. Type Assignment in the Lambda-Calculus: Syntax and Semantics. PhD thesis, University College of Swansea, September 1979. Google Scholar
  3. S. Broda and L. Damas. Counting a type’s (principal) inhabitants. Fundam. Inform., 45(1-2):33-51, 2001. Google Scholar
  4. S. Broda and L. Damas. On long normal inhabitants of a type. J. Log. and Comput., 15:353-390, June 2005. Google Scholar
  5. M.W. Bunder. Proof finding algorithms for implicational logics. Theoretical Computer Science, 232(1–2):165-186, 2000. Google Scholar
  6. Andrej Dudenhefner and Jakob Rehof. The complexity of principal inhabitation. In %2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, volume 84 of LIPIcs, pages 15:1-15:14, 2017. Google Scholar
  7. Silvia Ghilezan. Inhabitation in intersection and union type assignment systems. J. Log. Comput., 3(6):671-685, 1993. Google Scholar
  8. J.R. Hindley. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997. Google Scholar
  9. R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc, 146:29-60, December 1969. Google Scholar
  10. S. Hirokawa. Infiniteness of proof (α) is polynomial-space complete. Theor. Comput. Sci., 206(1-2):331-339, 1998. Google Scholar
  11. W.A. Howard. The formulas-as-types notion of construction. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479-490. Academic Press, 1980. Google Scholar
  12. Y. Komori and S. Hirokawa. The number of proofs for a BCK-formula. J. Symb. Log., 58(2):626-628, 1993. Google Scholar
  13. Aleksy Schubert, Wil Dekkers, and Hendrik Pieter Barendregt. Automata theoretic account of proof search. In CSL 2015, pages 128-143, 2015. Google Scholar
  14. R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci., 9:67-72, 1979. Google Scholar
  15. M. Takahashi, Y. Akama, and S. Hirokawa. Normal proofs and their grammar. Information and Computation, 125(2):144-153, 1996. Google Scholar
  16. P. Urzyczyn. Inhabitation in typed lambda-calculi (a syntactic approach). In TLCA'97, volume 1210 of LNCS, pages 373-389. Springer, 1997. Google Scholar