A framework for defining logics
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- A rewriting logic approach to operational semantics
- Proof assistants: history, ideas and future
- A notation for lambda terms. A generalization of environments
- Type checking with universes
- Dependent type system with subtyping I: Type level transitivity elimination
- From constructivism to computer science
- Implementing tactics and tacticals in a higher-order logic programming language
- Nominalization, predication and type containment
- Toward formal development of programs from algebraic specifications: Parameterisation revisited
- Structured theory presentations and logic representations
- Inductive families
- A higher-order unification algorithm for inductive types and dependent types
- A linear logical framework
- The calculus of constructions as a framework for proof search with set variable instantiation
- Proof-search in type-theoretic languages: An introduction
- Program development schemata as derived rules
- -calculus in (Co)inductive-type theory
- TWAM: a certifying abstract machine for logic programs
- A formalized general theory of syntax with bindings
- Making PVS accessible to generic services by interpretation in a universal format
- A semantic framework for proof evidence
- Binding operators for nominal sets
- Proof certificates for equality reasoning
- Canonical HybridLF: extending Hybrid with dependent types
- Amalgamation in the semantics of CASL
- Transitivity in coercive subtyping
- The foundation of a generic theorem prover
- Automated techniques for provably safe mobile code.
- Structural cut elimination. I: Intuitionistic and classical logic
- Higher-order substitutions
- On the formalization of the modal -calculus in the calculus of inductive constructions
- Dependent types with subtyping and late-bound overloading
- A note on the proof theory of the -calculus
- An approach to literate and structured formal developments
- Human rationality challenges universal logic
- Twenty years of rewriting logic
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
- The Mizar Mathematical Library in OMDoc: translation and applications
- Cut elimination for a logic with induction and co-induction
- Relative properties of frame language
- A formalized general theory of syntax with bindings: extended version
- Subformula linking for intuitionistic logic with application to type theory
- Harpoon: mechanizing metatheory interactively
- Experiences from exporting major proof assistant libraries
- The universal exponentiable arrow
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
- Logic-independent proof search in logical frameworks (short paper)
- From the universality of mathematical truth to the interoperability of proof systems
- Rensets and renaming-based recursion for syntax with bindings
- Semantical analysis of contextual types
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Structure-preserving diagram operators
- A type-theoretic approach to program development
- From LCF to Isabelle/HOL
- Mechanized metatheory revisited
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Mechanizing metatheory without typing contexts
- Strongly typed term representations in Coq
- A canonical locally named representation of binding
- Formalizing adequacy: a case study for higher-order abstract syntax
- A two-level logic approach to reasoning about computations
- Morphism axioms
- A framework for conflict analysis of normative texts written in controlled natural language
- SMT proof checking using a logical framework
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Proof checking and logic programming
- The future of logic: foundation-independence
- A higher-order calculus and theory abstraction
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
- Categorical properties of logical frameworks
- A higher-order abstract syntax approach to verified transformations on functional programs
- Explicit contexts in LF (extended abstract)
- Case analysis of higher-order data
- Reasoning in Abella about structural operational semantics specifications
- Developing (meta)theory of -calculus in the theory of contexts
- A representation of \(F_{\omega}\) in LF
- A third-order representation of the -calculus
- The theory of contexts for first order and higher order abstract syntax
- Comparing higher-order encodings in logical frameworks and tile logic
- A framework for defining logical frameworks
- Programmed strategies for program verification
- Functional programming with higher-order abstract syntax and explicit substitutions
- Hybridizing a logical framework
- Normalization for the simply-typed lambda-calculus in Twelf
- Meta-programming with built-in type equality
- Specifying properties of concurrent computations in CLF
- Redundancy elimination for LF
- A meta linear logical framework
- Imperative LF meta-programming
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Realizing the dependently typed -calculus
- A proof theoretic interpretation of model theoretic hiding
- Towards logical frameworks in the heterogeneous tool set Hets
- A query language for formal mathematical libraries
- Certificate size reduction in abstraction-carrying code
- Intuitionistic ancestral logic as a dependently typed abstract programming language
- Extensible Datasort Refinements
- Programs using syntax with first-class binders
- \textsc{Lincx}: a linear logical framework with first-class contexts
- The representational adequacy of Hybrid
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)
