Term-generic logic

DOI10.1016/j.tcs.2015.01.047zbMath1310.03044OpenAlexW2011407760MaRDI QIDQ2339466

Grigore Roşu, Andrei Popescu

Publication date: 1 April 2015

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2015.01.047

zbMATH Keywords

semantics\(\lambda\)-calculus\(\pi\)-calculussubstitutionterm-generic logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Related Items (6)

A formalized general theory of syntax with bindings ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Distilling the requirements of Gödel's incompleteness theorems with a proof assistant ⋮ A formally verified abstract account of Gödel's incompleteness theorems ⋮ Rensets and renaming-based recursion for syntax with bindings

Uses Software

• HYBRID
• Ott
• Isabelle/HOL
• PoplMark
• Nominal Isabelle

Cites Work

• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Linear logic
• Using typed lambda calculus to implement formal systems on a machine
• The semantics of second-order lambda calculus
• Nominal techniques in Isabelle/HOL
• External and internal syntax of the \(\lambda \)-calculus
• Substitution revisited
• A calculus of mobile processes. II
• An algebraic generalization of Frege structures -- binding algebras
• Isabelle/HOL. A proof assistant for higher-order logic
• The foundation of a generic theorem prover
• A canonical locally named representation of binding
• A two-level logic approach to reasoning about computations
• Term-Generic Logic
• Engineering formal metatheory
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
• Nominal Algebra and the HSP Theorem
• Logical relations and the typed λ-calculus
• Lambda‐Calculus Models and Extensionality
• Recursion principles for syntax with bindings and substitution
• Ott: Effective tool support for the working semanticist
• Mechanizing metatheory in a logical framework
• Completeness and Herbrand theorems for nominal logic
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• Reasoning with higher-order abstract syntax in a logical framework
• General Bindings and Alpha-Equivalence in Nominal Isabelle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Term-generic logic