Proof Systems for Retracts in Simply Typed Lambda Calculus

Colin Stirling

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationAutomata, Languages, and Programming
Subtitle of host publication40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II
EditorsFedor V. Fomin, Rusins Freivalds, Marta Kwiatkowska, David Peleg
PublisherSpringer-Verlag GmbH
Number of pages12
ISBN (Electronic)978-3-642-39212-2
ISBN (Print)978-3-642-39211-5
Publication statusPublished - 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Proof Systems for Retracts in Simply Typed Lambda Calculus'. Together they form a unique fingerprint.

Cite this