Proof Systems for Retracts in Simply Typed Lambda Calculus

  • Colin Stirling
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7966)


This paper concerns retracts in simply typed lambda calculus assuming βη-equality. We provide a simple tableau proof system which characterises when a type is a retract of another type and which leads to an exponential decision procedure.


Decision Procedure Product Rule Proof System Target Type Variable Node 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 118–309. Oxford University Press (1992)Google Scholar
  2. 2.
    Bruce, K., Longo, G.: Provable isomorphisms and domain equations in models of typed languages. In: Proc. 17th Symposium on Theory of Computing, pp. 263–272. ACM (1985)Google Scholar
  3. 3.
    de ’Liguoro, U., Piperno, A., Statman, R.: Retracts in simply typed λβη-calculus. In: Procs. LICS 1992, pp. 461–469 (1992)Google Scholar
  4. 4.
    Loader, R.: Higher-order β-matching is undecidable. Logic Journal of the IGPL 11(1), 51–68 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  5. 5.
    Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Procs. LICS 2006, pp. 81–90 (2006)Google Scholar
  6. 6.
    Ong, C.-H.L., Tzevelekos, N.: Functional Reachability. In: Procs. LICS 2009, pp. 286–295 (2009)Google Scholar
  7. 7.
    Padovani, V.: Decidability of fourth-order matching. Mathematical Structures in Computer Science 10(3), 361–372 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Padovani, V.: Retracts in simple types. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 376–384. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    Regnier, L., Urzyczyn, P.: Retractions of types with many atoms, pp. 1–16 (2005),
  10. 10.
    Schubert, A.: On the building of affine retractions. Math. Struct. in Comp. Science 18, 753–793 (2008)MathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    Stirling, C.: Higher-order matching, games and automata. In: Procs. LICS 2007, pp. 326–335 (2007)Google Scholar
  12. 12.
    Stirling, C.: Dependency tree automata. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 92–106. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  13. 13.
    Stirling, C.: Decidability of higher-order matching. Logical Methods in Computer Science 5(3:2), 1–52 (2009)MathSciNetGoogle Scholar
  14. 14.
    Stirling, C.: An introduction to decidability of higher-order matching (2012) (Submitted for Publication), Availble at author’s websiteGoogle Scholar
  15. 15.
    Vorobyov, S.: The “hardest” natural decidable theory. In: Procs. LICS 1997, pp. 294–305 (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Colin Stirling
    • 1
  1. 1.School of InformaticsUniversity of EdinburghUK

Personalised recommendations