Formal SOS-Proofs for the Lambda-Calculus

DOI10.1016/J.ENTCS.2009.07.053MaRDI QIDQ5178966zbMATH OpenOpenAlexFDO

Authors Christian Urban, Julien Narboux

Publication date 18 March 2015

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

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

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

zbMATH Keywords

\(\lambda\)-calculusNominal Isabelleproof assistantsstructural operational semantics

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1670575
• The \(\lambda \)-calculus and the unity of structural proof theory
• scientific article; zbMATH DE number 2134911
• THE Σλ-CALCULUS AND DERIVED PROGRAM FORMS
• A note on the proof theory of the -calculus
• A semantic characterization of the well-typed formulae of \(\lambda\)- calculus
• Theorem proving for untyped constructive -calculus: Implementation and application
• Reducibility Proofs in the λ-Calculus
• scientific article; zbMATH DE number 65536
• Typed Lambda Calculi and Applications

Cites work

• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• A structural approach to operational semantics
• Alpha-structural recursion and induction
• Automated Deduction – CADE-20
• Engineering formal metatheory
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• scientific article; zbMATH DE number 2238212 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Mechanizing the metatheory of LF
• Nominal Inversion Principles
• Nominal logic, a first order theory of names and binding
• Nominal techniques in Isabelle/HOL
• The lambda calculus, its syntax and semantics
• Theorem Proving in Higher Order Logics

Cited in

(4)

• Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
• A Formal Correspondence Between OMDoc with Alternative Proofs and the ${\overline{\lambda}\mu\tilde{\mu}}$ -Calculus
• Generic Authenticated Data Structures, Formally.
• Logical Relations for PCF

Describes a project that uses

Uses Software

• Isar
• Nominal Isabelle
• Isabelle/HOL

This page was built for publication: Formal SOS-Proofs for the Lambda-Calculus

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