A framework for defining logics
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Intuitionistic completeness of first-order logic
- Programs using syntax with first-class binders
- The rewriting logic semantics project: a progress report
- The practice of logical frameworks
- Reasoning in Abella about structural operational semantics specifications
- Logic representation in LF
- Proof search with set variable instantiation in the calculus of constructions
- Proving and rewriting
- The rewriting logic semantics project: a progress report
- scientific article; zbMATH DE number 7447767 (Why is no real title available?)
- The theory of contexts for first order and higher order abstract syntax
- Automated techniques for provably safe mobile code.
- Dependent types with subtyping and late-bound overloading
- Twenty years of rewriting logic
- A logical framework combining model and proof theory
- A type-theoretic approach to program development
- Definition and basic properties of the Deva meta-calculus
- Theo: An interactive proof development system
- scientific article; zbMATH DE number 7559275 (Why is no real title available?)
- The future of logic: foundation-independence
- A dependent type theory with abstractable names
- Structural cut elimination. I: Intuitionistic and classical logic
- From the universality of mathematical truth to the interoperability of proof systems
- Rensets and renaming-based recursion for syntax with bindings
- Scalable fine-grained proofs for formula processing
- A scalable module system
- Intuitionistic ancestral logic as a dependently typed abstract programming language
- A framework for proof systems
- Representing unification in a logical framework
- SpeX: a rewriting-based formal specification environment
- scientific article; zbMATH DE number 29052 (Why is no real title available?)
- Subformula linking for intuitionistic logic with application to type theory
- Math Literate Knowledge Management via Induced Material
- Unifying sets and programs via dependent types
- \textsc{Lincx}: a linear logical framework with first-class contexts
- Do-it-yourself type theory
- A practical implementation of simple consequence relations using inductive definitions
- Higher-order annotated terms for proof search
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- A rewriting logic approach to operational semantics
- Towards Knowledge Management for HOL Light
- Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
- Introduction to Type Theory
- Representing model theory in a type-theoretical logical framework
- scientific article; zbMATH DE number 7559294 (Why is no real title available?)
- The foundation of a generic theorem prover
- Substitution in non-wellfounded syntax with variable binding
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- Certificate size reduction in abstraction-carrying code
- Machine Translation and Type Theory
- Combining source, content, presentation, narration, and relational representation
- A general framework for the semantics of type theory
- Specifying properties of concurrent computations in CLF
- Binding operators for nominal sets
- Canonical HybridLF: extending Hybrid with dependent types
- On extensibility of proof checkers
- The Twelf Proof Assistant
- Mechanized metatheory revisited
- Formal logic definitions for interchange languages
- Least and greatest fixed points in intuitionistic natural deduction
- Structure-preserving diagram operators
- Simplifying proofs in Fitch-style natural deduction systems
- Dependent type system with subtyping I: Type level transitivity elimination
- A formalized general theory of syntax with bindings
- A framework for defining logical frameworks
- Programmed strategies for program verification
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- TWAM: a certifying abstract machine for logic programs
- Proof checking and logic programming
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- In praise of impredicativity: a contribution to the formalization of meta-programming
- Morphism axioms
- scientific article; zbMATH DE number 4164201 (Why is no real title available?)
- scientific article; zbMATH DE number 65533 (Why is no real title available?)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Proof checking and logic programming
- From constructivism to computer science
- Redundancy elimination for LF
- An induction principle for pure type systems
- Mechanizing metatheory in a logical framework
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules
- A proof theoretic interpretation of model theoretic hiding
- Towards logical frameworks in the heterogeneous tool set Hets
- Flexary operators for formalized mathematics
- A query language for formal mathematical libraries
- Proof-directed program transformation: a functional account of efficient regular expression matching
- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)
- A foundational view on integration problems
- A natural deduction approach to dynamic logic
- A formalized general theory of syntax with bindings: extended version
- Mechanizing metatheory without typing contexts
- Nominal abstraction
- Forum: A multiple-conclusion specification logic
- scientific article; zbMATH DE number 1231543 (Why is no real title available?)
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- A notation for lambda terms. A generalization of environments
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
- Term-Generic Logic
- Reflection of formal tactics in a deductive reflection framework
This page was built for publication: A framework for defining logics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4033837)
