- New
-
Topics
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- Journals
- Submit material
- More
Term-Space Semantics of Typed Lambda Calculus
Notre Dame Journal of Formal Logic 61 (4):591-600 (2020)
Abstract
Barendregt gave a sound semantics of the simple type assignment system λ → by generalizing Tait’s proof of the strong normalization theorem. In this paper, we aim to extend the semantics so that the completeness theorem holds.Links
PhilArchive
External links
(no proxy)
Setup an account with your affiliations in order to access resources via your University's proxy server
Through your library
- Sign in / register and customize your OpenURL resolver
- Configure custom resolver
My notes
Similar books and articles
Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms.Yuta Takahashi & Ryo Takemura - 2019 - Journal of Philosophical Logic 48 (3):553-570.
Strong Normalizability of Typed Lambda-Calculi for Substructural Logics.Motohiko Mouri & Norihiro Kamide - 2008 - Logica Universalis 2 (2):189-207.
The Church-Rosser theorem for the typed $\lambda$-calculus with surjective pairing.Garrel Pottinger - 1981 - Notre Dame Journal of Formal Logic 22 (3):264-268.
Weak typed Böhm theorem on IMLL.Satoshi Matsuoka - 2007 - Annals of Pure and Applied Logic 145 (1):37-90.
Proofs of the normalization and Church-Rosser theorems for the typed $\lambda$-calculus.Garrel Pottinger - 1978 - Notre Dame Journal of Formal Logic 19 (3):445-451.
A completeness result for the simply typed λμ-calculus.Karim Nour & Khelifa Saber - 2010 - Annals of Pure and Applied Logic 161 (1):109-118.
Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations.Sara Ayhan - forthcoming - Journal of Logic and Computation.
The judgement calculus for intuitionistic linear logic: Proof theory and semantics.Silvio Valentini - 1992 - Mathematical Logic Quarterly 38 (1):39-58.
Completeness and partial soundness results for intersection and union typing for λ ¯ μ μ ̃.Steffen van Bakel - 2010 - Annals of Pure and Applied Logic 161 (11):1400-1430.
Light affine lambda calculus and polynomial time strong normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Analytics
Added to PP
2020-12-31
Downloads
19 (#791,817)
6 months
6 (#701,126)
2020-12-31
Downloads
19 (#791,817)
6 months
6 (#701,126)
Historical graph of downloads
References found in this work
Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
A Filter lambda model and the completeness of type assignment.Henk Barendregt, Mario Coppo & Mariangiola Dezani-Ciancaglini - 1983 - Journal of Symbolic Logic 48 (4):931-940.
Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-6686886f5-7g5mb uwo