Twelf
From MaRDI portal
Software:18957
No author found.
Related Items (only showing first 100 items - show all)
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving ⋮ Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ Towards Logical Frameworks in the Heterogeneous Tool Set Hets ⋮ The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ GMeta: A Generic Formal Metatheory Framework for First-Order Representations ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ Proof checking and logic programming ⋮ Generic Literals ⋮ Formal Logic Definitions for Interchange Languages ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Inductive Beluga: Programming Proofs ⋮ Extending MKM Formats at the Statement Level ⋮ Implementing Cantor’s Paradise ⋮ There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners ⋮ Verifying termination and reduction properties about higher-order logic programs ⋮ Unnamed Item ⋮ A canonical locally named representation of binding ⋮ A two-level logic approach to reasoning about computations ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics ⋮ The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 ⋮ A language-based approach to functionally correct imperative programming ⋮ Programming Type-Safe Transformations Using Higher-Order Abstract Syntax ⋮ System F in Agda, for fun and profit ⋮ Higher-order term indexing using substitution trees ⋮ Mechanizing the metatheory of LF ⋮ Logical relations for a logical framework ⋮ Structural Focalization ⋮ A scalable module system ⋮ Intuitionistic completeness of first-order logic ⋮ Constraint solving in non-permutative nominal abstract syntax ⋮ Nominal abstraction ⋮ A linear logical framework ⋮ A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. ⋮ A formal framework for specifying sequent calculus proof systems ⋮ The Mizar Mathematical Library in OMDoc: translation and applications ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ A list-machine benchmark for mechanized metatheory ⋮ A semantic framework for proof evidence ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory ⋮ Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Disjoint intersection types ⋮ Representing model theory in a type-theoretical logical framework ⋮ Extensible Datasort Refinements ⋮ Programs Using Syntax with First-Class Binders ⋮ LINCX: A Linear Logical Framework with First-Class Contexts ⋮ The Abella Interactive Theorem Prover (System Description) ⋮ Celf – A Logical Framework for Deductive and Concurrent Systems (System Description) ⋮ Higher-Order Dynamic Pattern Unification for Dependent Types and Records ⋮ A formalized general theory of syntax with bindings: extended version ⋮ A Coverage Checking Algorithm for LF ⋮ Canonical HybridLF: extending Hybrid with dependent types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Towards MKM in the Large: Modular Representation and Scalable Software Architecture ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Programming Inductive Proofs ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory ⋮ Visible Type Application ⋮ Automatically Splitting a Two-Stage Lambda Calculus ⋮ On the effectiveness of higher-order logic programming in language-oriented programming ⋮ A treatment of higher-order features in logic programming ⋮ On the Expressivity of Minimal Generic Quantification ⋮ Explicit Contexts in LF (Extended Abstract) ⋮ Case Analysis of Higher-Order Data ⋮ Reasoning in Abella about Structural Operational Semantics Specifications ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Lem: A Lightweight Tool for Heavyweight Semantics ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Harpoon: mechanizing metatheory interactively ⋮ Mechanizing the Metatheory of mini-XQuery ⋮ Realizing the Dependently Typed Lambda Calculus. ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Mechanized metatheory revisited ⋮ Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. ⋮ A Representation of Fω in LF ⋮ A Third-Order Representation of the λμ-Calculus ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic ⋮ Automated techniques for provably safe mobile code. ⋮ Ruler: Programming Type Rules ⋮ A Framework for Defining Logical Frameworks ⋮ Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions ⋮ Type-level Computation Using Narrowing in Ωmega ⋮ Language-Based Program Verification via Expressive Types ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ Hybridizing a Logical Framework ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Normalization for the Simply-Typed Lambda-Calculus in Twelf ⋮ A Logical Framework with Explicit Conversions ⋮ Meta-programming With Built-in Type Equality ⋮ Imperative LF Meta-Programming ⋮ Mechanizing metatheory without typing contexts ⋮ The future of logic: foundation-independence
This page was built for software: Twelf
