Twelf
From MaRDI portal
Software:18957
swMATH6888MaRDI QIDQ18957FDOQ18957
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Intuitionistic completeness of first-order logic
- A logical framework combining model and proof theory
- Project Abstract: Logic Atlas and Integrator (LATIN)
- The future of logic: foundation-independence
- Lax Theory Morphisms
- Building reliable, high-performance networks with the Nuprl proof development system
- Title not available (Why is that?)
- A scalable module system
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
- A Linear Spine Calculus
- Contextual modal type theory
- Representing model theory in a type-theoretical logical framework
- Termination checking with types
- Proof Pearl: Abella Formalization of λ-Calculus Cube Property
- Encoding functional relations in Scunak
- A synthesis of the procedural and declarative styles of interactive theorem proving
- A language-based approach to functionally correct imperative programming
- Title not available (Why is that?)
- A framework for defining logical frameworks
- Towards proof planning for \(\mathcal{M}_{\omega}^+\)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
- Proof checking and logic programming
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- A formal framework for specifying sequent calculus proof systems
- Mechanizing metatheory in a logical framework
- The Abella Interactive Theorem Prover (System Description)
- Ruler: Programming Type Rules
- Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Linearity Constraints as Bounded Intervals in Linear Logic Programming
- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)
- A formalized general theory of syntax with bindings: extended version
- Nominal abstraction
- Automated Deduction – CADE-19
- General bindings and alpha-equivalence in Nominal Isabelle
- Verifying termination and reduction properties about higher-order logic programs
- The Mizar Mathematical Library in OMDoc: translation and applications
- N. G. de Bruijn's contribution to the formalization of mathematics
- A canonical locally named representation of binding
- Dependent types ensure partial correctness of theorem provers
- Title not available (Why is that?)
- A linear logical framework
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- An Interpretation of Isabelle/HOL in HOL Light
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
- Ott
- Realizing the dependently typed \(\lambda\)-calculus
- Type-level computation using narrowing in \(\Omega\)mega
- Higher-order abstract syntax in type theory
- Towards Logical Frameworks in the Heterogeneous Tool Set Hets
- Extending MKM Formats at the Statement Level
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
- Language-based program verification via expressive types
- Title not available (Why is that?)
- Theorem Proving in Higher Order Logics
- $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
- Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
- Isabelle's metalogic: formalization and proof checker
- Elaborating intersection and union types
- A formalization and proof checker for Isabelle's metalogic
- Towards MKM in the Large: Modular Representation and Scalable Software Architecture
- TPS: A hybrid automatic-interactive system for developing proofs
- Verifying and Invalidating Textbook Proofs Using Scunak
- An Effect System for Algebraic Effects and Handlers
- A two-level logic approach to reasoning about computations
- Generic Literals
- A list-machine benchmark for mechanized metatheory
- Computer Science Logic
- Proof Checking and Logic Programming
- An Improved Proof-Theoretic Compilation of Logic Programs
- Case analysis of higher-order data
- Explicit contexts in LF (extended abstract)
- On the expressivity of minimal generic quantification
- A hybrid encoding of Howe's method for establishing congruence of bisimilarity
- Title not available (Why is that?)
- A Formal Calculus for Informal Equality with Binding
- Programming Inductive Proofs
- Automated Deduction – CADE-19
- A Coverage Checking Algorithm for LF
- Title not available (Why is that?)
- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
- Reasoning in Abella about structural operational semantics specifications
- Flexary Operators for Formalized Mathematics
- Automated techniques for provably safe mobile code.
- A case study in programming coinductive proofs: Howe’s method
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Rensets and renaming-based recursion for syntax with bindings
- Theorem Proving in Higher Order Logics
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Automated Deduction – CADE-19
- Mechanized metatheory revisited
- Canonical HybridLF: extending Hybrid with dependent types
- Functions-as-constructors higher-order unification: extended pattern unification
- GMeta: A Generic Formal Metatheory Framework for First-Order Representations
- Programs Using Syntax with First-Class Binders
This page was built for software: Twelf
