Formal SOS-Proofs for the Lambda-Calculus

DOI10.1016/j.entcs.2009.07.053zbMath1310.68184OpenAlexW2018100734MaRDI QIDQ5178966

Christian Urban, Julien Narboux

Publication date: 18 March 2015

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.2009.07.053

zbMATH Keywords

structural operational semantics\(\lambda\)-calculusproof assistantsNominal Isabelle

Mathematics Subject Classification ID

Related Items (1)

Generic Authenticated Data Structures, Formally.

Uses Software

• Isabelle/HOL
• Isar
• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nominal techniques in Isabelle/HOL
• The lambda calculus, its syntax and semantics
• Isabelle/HOL. A proof assistant for higher-order logic
• A structural approach to operational semantics
• Nominal logic, a first order theory of names and binding
• Mechanizing the metatheory of LF
• Engineering formal metatheory
• Nominal Inversion Principles
• Alpha-structural recursion and induction
• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
• Automated Deduction – CADE-20
• Theorem Proving in Higher Order Logics

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