Proof Systems for Retracts in Simply Typed Lambda Calculus

Colin Stirling

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

Abstract

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
Pages398-409
Number of pages12
ISBN (Electronic)978-3-642-39212-2
ISBN (Print)978-3-642-39211-5
DOIs
Publication statusPublished - 2013

Publication series

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

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

Cite this