LIPIcs.CSL.2013.634.pdf
- Filesize: 324 kB
- 19 pages
Document
A New Type Assignment for Strongly Normalizable Terms
Author
-
Part of:
Volume:
Computer Science Logic 2013 (CSL 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2013-09-02
Cite As Get BibTex
Rick Statman. A New Type Assignment for Strongly Normalizable Terms. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 634-652, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.CSL.2013.634
Abstract
We consider an operator definable in the intuitionistic theory of monadic predicates and we axiomatize some of its properties in a definitional extension of that monadic logic. The axiomatization lends itself to a natural deduction formulation to which the Curry-Howard isomorphism can be applied. The resulting Church style type system has the property that an untyped term is typable if and only if it is strongly normalizable.
Subject Classification
Keywords
- lambda calculus
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads