Kripke-style Semantics and Completeness for Full Simply Typed Lambda Calculus

2020 ◽  
Vol 30 (8) ◽  
pp. 1567-1608
Author(s):  
Simona Kašterović ◽  
Silvia Ghilezan
Keyword(s):  
Lambda Calculus ◽  
Canonical Model ◽  
Typed Lambda Calculus ◽  
Type Assignment ◽  
Soundness And Completeness

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.

scholarly journals Kripke Semantics for Intersection Formulas

2021 ◽  
Vol 22 (3) ◽  
pp. 1-16
Author(s):  
Andrej Dudenhefner ◽  
Paweł Urzyczyn
Keyword(s):  
Kripke Semantics ◽  
Type Assignment ◽  
Soundness And Completeness

We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced in every model. As a by-product, we obtain another proof of normalization for the Barendregt–Coppo–Dezani intersection type assignment system.

scholarly journals Backpropagation in the simply typed lambda-calculus with linear negation

2020 ◽  
Vol 4 (POPL) ◽  
pp. 1-27 ◽  
Author(s):  
Aloïs Brunel ◽  
Damiano Mazza ◽  
Michele Pagani
Keyword(s):  
Lambda Calculus ◽  
Typed Lambda Calculus

The Simply Typed Lambda Calculus

2013 ◽  
pp. 5-54
Author(s):  
Henk Barendregt ◽  
Wil Dekkers ◽  
Richard Statman
Keyword(s):  
Lambda Calculus ◽  
Typed Lambda Calculus
Sign in / Sign up

Export Citation Format

Share Document