Syntactic Logical Relations for Polymorphic and Recursive Types

DOI10.1016/j.entcs.2007.02.010zbMath1277.68119OpenAlexW1992889841MaRDI QIDQ2864153

Karl Crary, Robert Harper

Publication date: 6 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.02.010

zbMATH Keywords

operational semanticspolymorphismtype structuredata abstractionlogics of programslambda calculus and related systems

Mathematics Subject Classification ID

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

Related Items (12)

On the Versatility of Open Logical Relations ⋮ A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go ⋮ Semantic preservation for a type directed translation scheme of Featherweight Go ⋮ Correctness of compiling polymorphism to dynamic typing ⋮ Parametricity, type equality, and higher-order polymorphism ⋮ Realisability semantics of parametric polymorphism, general references and recursive types ⋮ Typing termination in a higher-order concurrent imperative language ⋮ Exception tracking in an open world ⋮ Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types ⋮ A family of syntactic logical relations for the semantics of Haskell-like languages ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ Free Theorems and Runtime Type Representations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the relations between monadic semantics
• LCF considered as a programming language
• Relational interpretations of recursive types in an operational setting.
• The origins of structural operational semantics
• A structural approach to operational semantics
• Proving congruence of bisimulation in functional programming languages
• From operational semantics to domain theory
• Relational properties of domains
• Proof of correctness of data representations
• Semantic types
• Logical relations and the typed λ-calculus
• The Category-Theoretic Solution of Recursive Domain Equations
• Parametric polymorphism and operational equivalence
• A bisimulation for type abstraction and recursion
• Programming Languages and Systems

This page was built for publication: Syntactic Logical Relations for Polymorphic and Recursive Types