Constructing type systems over an operational semantics

DOI10.1016/0747-7171(92)90026-ZzbMath0766.68088MaRDI QIDQ1199709

Robert Harper

Publication date: 16 January 1993

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

operational semanticspartial equivalence relationstype systemMartin-Löf's type theoryinductive definitiontype-free programming language

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Second- and higher-order arithmetic and fragments (03F35)

Related Items

Unnamed Item, MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK

Uses Software

• ML
• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The semantics of second-order lambda calculus
• Intuitionism. An introduction
• The calculus of constructions
• The lambda calculus, its syntax and semantics
• A theory of type polymorphism in programming
• Computational foundations of basic recursive function theory
• The completeness theorem for typing lambda-terms
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Combinatory logic. Vol. II
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• Constructive mathematics and computer programming
• Recursive models for constructive set theories
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• On the Semantics of “Data Type”
• Intensional interpretations of functionals of finite type I
• The Principal Type-Scheme of an Object in Combinatory Logic