Constructing type systems over an operational semantics

DOI10.1016/0747-7171(92)90026-ZMaRDI QIDQ1199709zbMATH OpenFDO

Authors Robert Harper

Publication date 16 January 1993

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

zbMATH Keywords

type systemoperational semanticsinductive definitionpartial equivalence relationstype-free programming languageMartin-Löf's type theory

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2077110
• scientific article; zbMATH DE number 3881865
• Semantics of constructions. I: The traditional approach
• Do-it-yourself type theory
• scientific article; zbMATH DE number 2185661

Cites work

• scientific article; zbMATH DE number 3829227 (Why is no real title available?)
• scientific article; zbMATH DE number 3928338 (Why is no real title available?)
• scientific article; zbMATH DE number 3928956 (Why is no real title available?)
• scientific article; zbMATH DE number 3930968 (Why is no real title available?)
• scientific article; zbMATH DE number 4049615 (Why is no real title available?)
• scientific article; zbMATH DE number 3722625 (Why is no real title available?)
• scientific article; zbMATH DE number 3726339 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 3485716 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 3557754 (Why is no real title available?)
• scientific article; zbMATH DE number 4187810 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A filter lambda model and the completeness of type assignment
• A new type assignment for λ-terms
• A theory of type polymorphism in programming
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Combinatory logic. Vol. II
• Computational foundations of basic recursive function theory
• Constructive mathematics and computer programming
• Intensional interpretations of functionals of finite type I
• Intuitionism. An introduction
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On the Semantics of “Data Type”
• Recursive models for constructive set theories
• The Principal Type-Scheme of an Object in Combinatory Logic
• The calculus of constructions
• The completeness theorem for typing lambda-terms
• The lambda calculus, its syntax and semantics
• The semantics of second-order lambda calculus

Cited in

(8)

• scientific article; zbMATH DE number 3881865 (Why is no real title available?)
• A two-storied universe of transfinite mechanisms
• Formalizing type operations using the ``image type constructor
• Native type theory
• Semantics of constructions. I: The traditional approach
• scientific article; zbMATH DE number 7566056 (Why is no real title available?)
• scientific article; zbMATH DE number 2185661 (Why is no real title available?)
• Martin-Löf's type theory as an open-ended framework

Describes a project that uses

Uses Software

• Nuprl
• ML

This page was built for publication: Constructing type systems over an operational semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1199709)