Paper Info
Title
Kripke-Style Semantics And Completeness For Full Simply Typed Lambda Calculus
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.
Year
DOI
Venue
2020
10.1093/logcom/exaa055
JOURNAL OF LOGIC AND COMPUTATION
Keywords
DocType
Volume
lambda calculus, Kripke-style semantics, completeness, Curry-Howard correspondence
Journal
30
Issue
ISSN
Citations 
8
0955-792X
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
Simona Kasterovic100.34
Silvia Ghilezan210614.66