Proof Systems for Retracts in Simply Typed Lambda Calculus

Colin Stirling

doi:10.1007/978-3-642-39212-2_36

Proof Systems for Retracts in Simply Typed Lambda Calculus

Colin Stirling

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Automata, Languages, and Programming
Subtitle of host publication	40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II
Editors	Fedor V. Fomin, Rusins Freivalds, Marta Kwiatkowska, David Peleg
Publisher	Springer-Verlag GmbH
Pages	398-409
Number of pages	12
ISBN (Electronic)	978-3-642-39212-2
ISBN (Print)	978-3-642-39211-5
DOIs	https://doi.org/10.1007/978-3-642-39212-2_36
Publication status	Published - 2013

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	7966
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-642-39212-2_36

stirling_proof_systemsAccepted author manuscript, 199 KB

http://link.springer.com/chapter/10.1007%2F978-3-642-39212-2_36

Cite this

Stirling, C. (2013). Proof Systems for Retracts in Simply Typed Lambda Calculus. In F. V. Fomin, R. Freivalds, M. Kwiatkowska, & D. Peleg (Eds.), Automata, Languages, and Programming: 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II (pp. 398-409). (Lecture Notes in Computer Science; Vol. 7966). Springer-Verlag GmbH. https://doi.org/10.1007/978-3-642-39212-2_36

@inproceedings{79ed3ca6bd3c4e35bedacd7597f8fda2,

title = "Proof Systems for Retracts in Simply Typed Lambda Calculus",

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.",

author = "Colin Stirling",

year = "2013",

doi = "10.1007/978-3-642-39212-2_36",

language = "English",

isbn = "978-3-642-39211-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag GmbH",

pages = "398--409",

editor = "Fomin, {Fedor V.} and Rusins Freivalds and Marta Kwiatkowska and David Peleg",

booktitle = "Automata, Languages, and Programming",

}

Stirling, C 2013, Proof Systems for Retracts in Simply Typed Lambda Calculus. in FV Fomin, R Freivalds, M Kwiatkowska & D Peleg (eds), Automata, Languages, and Programming: 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II. Lecture Notes in Computer Science, vol. 7966, Springer-Verlag GmbH, pp. 398-409. https://doi.org/10.1007/978-3-642-39212-2_36

Proof Systems for Retracts in Simply Typed Lambda Calculus. / Stirling, Colin.

Automata, Languages, and Programming: 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II. ed. / Fedor V. Fomin; Rusins Freivalds; Marta Kwiatkowska; David Peleg. Springer-Verlag GmbH, 2013. p. 398-409 (Lecture Notes in Computer Science; Vol. 7966).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Proof Systems for Retracts in Simply Typed Lambda Calculus

AU - Stirling, Colin

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-39212-2_36

DO - 10.1007/978-3-642-39212-2_36

M3 - Conference contribution

SN - 978-3-642-39211-5

T3 - Lecture Notes in Computer Science

SP - 398

EP - 409

BT - Automata, Languages, and Programming

A2 - Fomin, Fedor V.

A2 - Freivalds, Rusins

A2 - Kwiatkowska, Marta

A2 - Peleg, David

PB - Springer-Verlag GmbH

ER -

Stirling C. Proof Systems for Retracts in Simply Typed Lambda Calculus. In Fomin FV, Freivalds R, Kwiatkowska M, Peleg D, editors, Automata, Languages, and Programming: 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II. Springer-Verlag GmbH. 2013. p. 398-409. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-39212-2_36

Proof Systems for Retracts in Simply Typed Lambda Calculus

Abstract

Publication series

Access to Document

Fingerprint

Cite this