Typed operational semantics

DOI10.1007/BFB0014053MaRDI QIDQ3024835zbMATH OpenFDO

Authors Healfdene Goguen

Publication date 4 July 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0014053

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• Typed operational semantics for dependent record types
• Soundness of the logical framework for its typed operational semantics. Extended abstract
• scientific article; zbMATH DE number 3854393
• Typed -calculus with recursive definitions
• Constructing type systems over an operational semantics

Cited in

(13)

• Constructing type systems over an operational semantics
• Typed operational semantics for higher-order subtyping.
• Type theory should eat itself
• Strong normalization with singleton types
• Normalization for the simply-typed lambda-calculus in Twelf
• Soundness of the logical framework for its typed operational semantics. Extended abstract
• Typed operational semantics for dependent record types
• Taming the merge operator
• POPLMark reloaded: mechanizing proofs by logical relations
• An operational semantics for TOOPLE: A statically-typed object-oriented programming language
• The metatheory of UTT
• Type-directed operational semantics for gradual typing
• Strong Normalization of Moggis's Computational Metalanguage

This page was built for publication: Typed operational semantics

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