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. © 2013 Springer-Verlag.
CITATION STYLE
Stirling, C. (2013). Proof systems for retracts in simply typed lambda calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7966 LNCS, pp. 398–409). https://doi.org/10.1007/978-3-642-39212-2_36
Mendeley helps you to discover research relevant for your work.