Twelf

swMATH6888MaRDI QIDQ18957FDOQ18957

Author name not available (Why is that?)

Described by source

• The Twelf Proof Assistant
• Functional and Logic Programming

Cited In (only showing first 100 items - show all)

• 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
• First-Order Logic with Dependent Types
• Mechanizing metatheory without typing contexts
• Structural Focalization
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
• Mechanizing the metatheory of LF
• LINCX: A Linear Logical Framework with First-Class Contexts
• \(\mathrm{HO}\pi\) in Coq
• Automatically Splitting a Two-Stage Lambda Calculus
• Visible Type Application
• The calculus of dependent lambda eliminations
• Programming Type-Safe Transformations Using Higher-Order Abstract Syntax
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts
• Hybridizing a logical framework
• On the effectiveness of higher-order logic programming in language-oriented programming
• Meta-programming with built-in type equality
• Title not available (Why is that?)
• Higher-Order Dynamic Pattern Unification for Dependent Types and Records
• A list-machine benchmark for mechanized metatheory (extended abstract)
• Formal Logic Definitions for Interchange Languages
• Title not available (Why is that?)
• Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
• αCheck: A mechanized metatheory model checker
• Title not available (Why is that?)
• Title not available (Why is that?)
• On equivalence and canonical forms in the LF type theory
• System F in Agda, for fun and profit
• A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL
• A representation of \(F_{\omega}\) in LF
• Producing proofs from an arithmetic decision procedure in elliptical LF
• Constraint solving in non-permutative nominal abstract syntax
• A third-order representation of the \(\lambda\mu\)-calculus
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Semantics of Mizar as an Isabelle object logic
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• A semantic framework for proof evidence
• In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming
• 2-Dimensional Directed Type Theory
• Automating Theorem Proving with SMT
• Harpoon: mechanizing metatheory interactively
• Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative
• Inductive Beluga: Programming Proofs
• Functions-as-constructors Higher-order Unification
• No value restriction is needed for algebraic effects and handlers
• Formalizing Operational Semantic Specifications in Logic
• Higher-order term indexing using substitution trees
• 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?)
• 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

This page was built for software: Twelf