scientific article
From MaRDI portal
Publication:3024831
zbMath1063.68650MaRDI QIDQ3024831
Joëlle Desperyroux, Amy P. Felty, Andre Hirschowitz
Publication date: 4 July 2005
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items
LF+ in Coq for "fast and loose" reasoning, Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding, Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs, An initial algebra approach to term rewriting systems with variable binders, Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts, A two-level logic approach to reasoning about computations, A formalized general theory of syntax with bindings, A Survey of the Proof-Theoretic Foundations of Logic Programming, Rensets and renaming-based recursion for syntax with bindings extended version, Mechanizing type environments in weak HOAS, POPLMark reloaded: Mechanizing proofs by logical relations, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Nominal techniques in Isabelle/HOL, A formalized general theory of syntax with bindings: extended version, Canonical HybridLF: extending Hybrid with dependent types, \(\mathrm{HO}\pi\) in Coq, Primitive recursion for higher-order abstract syntax, Syntax for Free: Representing Syntax with Binding Using Parametricity, Mechanized metatheory revisited, Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types., The Theory of Contexts for First Order and Higher Order Abstract Syntax, Formalization of metatheory of the Quipper quantum programming language in a linear logic, Mechanizing focused linear logic in Coq, \(\pi\)-calculus in (Co)inductive-type theory, Structural cut elimination. I: Intuitionistic and classical logic, On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions, Rensets and renaming-based recursion for syntax with bindings, A Coq Library for Verification of Concurrent Programs, A focused linear logical framework and its application to metatheory of object logics, The practice of logical frameworks
Uses Software
