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 Letcc via Labelled Deduction
• Title not available (Why is that?)
• There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• Title not available (Why is that?)
• Lem: A Lightweight Tool for Heavyweight Semantics
• Mechanizing the Metatheory of mini-XQuery
• Logical relations for a logical framework
• Verification, Model Checking, and Abstract Interpretation
• Theorem Proving in Higher Order Logics
• A treatment of higher-order features in logic programming
• Disjoint intersection types
• Extensible Datasort Refinements
• Producing Certified Functional Code from Inductive Specifications
• Implementing Cantor’s Paradise
• Efficient Substitution in Hoare Logic Expressions
• Combining Source, Content, Presentation, Narration, and Relational Representation
• Functional programming with higher-order abstract syntax and explicit substitutions
• Proof-term synthesis on dependent-type systems via explicit substitutions
• A logical framework with explicit conversions
• A bidirectional refinement type system for LF
• Imperative LF meta-programming
• Normalization for the simply-typed lambda-calculus in Twelf
• 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

This page was built for software: Twelf