Authors: Kašterović, Simona
Ghilezan, Silvia 
Affiliations: Mathematics 
Mathematical Institute of the Serbian Academy of Sciences and Arts 
Title: Kripke-style semantics and completeness for full simply typed Lambda calculus
Journal: Journal of Logic and Computation
Volume: 30
Issue: 8
First page: 1567
Last page: 1608
Issue Date: 1-Jan-2021
Rank: ~M21
ISSN: 0955-792X
DOI: 10.1093/LOGCOM/EXAA055
Abstract: 
Full simply typed lambda calculus is the simply typed lambda calculus extended with product types and sum types. We propose a Kripke-style semantics for full simply typed lambda calculus. We then prove soundness and completeness of type assignment in full simply typed lambda calculus with respect to the proposed semantics. The key point in the proof of completeness is the notion of a canonical model.
Keywords: Completeness | Curry-Howard correspondence | Kripke-style semantics | Lambda calculus
Publisher: Oxford Academic Press

Show full item record

SCOPUSTM   
Citations

2
checked on Nov 27, 2022

Page view(s)

43
checked on Nov 27, 2022

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.