scientific article; zbMATH DE number 1754648
From MaRDI portal
Publication:4535076
Recommendations
- Foundations for the formalization of metamathematics and axiomatizations of consequence theories
- Effective Axiomatizations of Hoare Logics
- Nominal reasoning techniques in Coq (extended abstract)
- A Foundation for Metareasoning Part I: The Proof Theory
- Metalogic of intuitionistic propositional calculus
- scientific article; zbMATH DE number 2204757
- A family of metainferential logics
- Formalizing the meta-theory of first-order predicate logic
- Reasoning about reasoning in a meta-level architecture
Cited in
(15)- Nominal unification
- Nominal logic, a first order theory of names and binding
- Nested abstract syntax in Coq
- Semantical analysis of contextual types
- Fresh logic: Proof-theory and semantics for FM and nominal techniques
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- A first-order syntax for the -calculus in Isabelle/HOL using permutations
- Developing (meta)theory of -calculus in the theory of contexts
- The theory of contexts for first order and higher order abstract syntax
- Comparing higher-order encodings in logical frameworks and tile logic
- Nominal reasoning techniques in Coq (extended abstract)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- About permutation algebras, (pre)sheaves and named sets
- Mechanizing type environments in weak HOAS
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4535076)