Syntactic logical relations for polymorphic and recursive types

DOI10.1016/J.ENTCS.2007.02.010zbMATH Open1277.68119OpenAlexW1992889841MaRDI QIDQ2864153FDOQ2864153

Authors: 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

Recommendations

• Relational interpretations of recursive types in an operational setting.
• Parametric polymorphism and operational equivalence
• scientific article; zbMATH DE number 1231605
• Programming Languages and Systems
• scientific article; zbMATH DE number 3902022

zbMATH Keywords

polymorphismdata abstractionoperational semanticslogics of programstype structurelambda calculus and related systems

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (22)

• A case study in programming coinductive proofs: Howe’s method
• Correctness of compiling polymorphism to dynamic typing
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• Free Theorems and Runtime Type Representations
• A fibrational tale of operational logical relations: pure, effectful and differential
• Title not available (Why is that?)
• Logical relations for monadic types
• Title not available (Why is that?)
• Exception tracking in an open world
• Combinatory logic with polymorphic types
• Title not available (Why is that?)
• Polymorphic type inference for the relational algebra
• A family of syntactic logical relations for the semantics of Haskell-like languages
• A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go
• On the Versatility of Open Logical Relations
• Semantic preservation for a type directed translation scheme of Featherweight Go
• Relational interpretations of recursive types in an operational setting.
• Realisability semantics of parametric polymorphism, general references and recursive types
• Typing termination in a higher-order concurrent imperative language
• Parametricity, type equality, and higher-order polymorphism
• Programming Languages and Systems
• Programming Languages and Systems

This page was built for publication: Syntactic logical relations for polymorphic and recursive types

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