Mechanizing logical relations

DOI10.1007/3-540-58027-1_18MaRDI QIDQ5890057zbMATH OpenOpenAlexFDO

Authors Allen Stoughton

Publication date 28 April 2023

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

Full work available at URL https://doi.org/10.1007/3-540-58027-1_18

zbMATH Keywords

logical relationlambda calculusalgorithm schemaclosure processtype frame

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Logical relations and the typed λ-calculus
• scientific article; zbMATH DE number 3902022
• scientific article; zbMATH DE number 512784
• Mechanizing proofs with logical relations -- Kripke-style
• Logical relations for monadic types

Cites work

• scientific article; zbMATH DE number 431771 (Why is no real title available?)
• scientific article; zbMATH DE number 512783 (Why is no real title available?)
• scientific article; zbMATH DE number 512784 (Why is no real title available?)
• scientific article; zbMATH DE number 1142318 (Why is no real title available?)
• scientific article; zbMATH DE number 234028 (Why is no real title available?)
• LCF considered as a programming language

Cited in

(9)

• Degrees of parallelism in the continuous type hierarchy
• Relative definability of boolean functions via hypergraphs
• Computer Science Logic
• Linear Läuchli semantics
• Full abstraction for the second order subset of an Algol-like language
• Definability and full abstraction
• scientific article; zbMATH DE number 176729 (Why is no real title available?)
• Mechanizing Logic. II: Automated map logic method for relational arguments on paper and by computer
• On the expressive power of first-order boolean functions in PCF

This page was built for publication: Mechanizing logical relations

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