A New Type Assignment for Strongly Normalizable Terms

Author Rick Statman



PDF
Thumbnail PDF

File

LIPIcs.CSL.2013.634.pdf
  • Filesize: 324 kB
  • 19 pages

Document Identifiers

Author Details

Rick Statman

Cite AsGet 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.
Keywords
  • lambda calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail