Barendregt’s Variable Convention in Rule Inductions

DOI10.1007/978-3-540-73595-3_4zbMath1213.03024OpenAlexW2113705064MaRDI QIDQ3608761

Stefan Berghofer, Christian Urban, Michael Norrish

Publication date: 6 March 2009

Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_4

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items

The Role of Indirections in Lazy Natural Semantics, A canonical locally named representation of binding, Formalizing adequacy: a case study for higher-order abstract syntax, A formalized general theory of syntax with bindings, Rensets and renaming-based recursion for syntax with bindings extended version, A solution to the PoplMark challenge based on de Bruijn indices, Psi-calculi in Isabelle, Psi-calculi in Isabelle, Nominal techniques in Isabelle/HOL, Nominal Inversion Principles, A formalized general theory of syntax with bindings: extended version, External and internal syntax of the \(\lambda \)-calculus, On the Role of Names in Reasoning about λ-tree Syntax Specifications, Mechanizing the Metatheory of mini-XQuery, Rensets and renaming-based recursion for syntax with bindings, Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

Uses Software

• Isar