The following pages link to Twelf (Q18957):
Displaying 50 items.
- Producing proofs from an arithmetic decision procedure in elliptical LF (Q2844808) (← links)
- A hybrid encoding of Howe's method for establishing congruence of bisimilarity (Q2844810) (← links)
- Towards proof planning for \(\mathcal{M}_{\omega}^+\) (Q2844813) (← links)
- A framework for defining logical frameworks (Q2864157) (← links)
- Functional programming with higher-order abstract syntax and explicit substitutions (Q2866332) (← links)
- Type-level computation using narrowing in \(\Omega\)mega (Q2866338) (← links)
- Language-based program verification via expressive types (Q2866340) (← links)
- Hybridizing a logical framework (Q2867954) (← links)
- Normalization for the simply-typed lambda-calculus in Twelf (Q2871835) (← links)
- A logical framework with explicit conversions (Q2871837) (← links)
- Meta-programming with built-in type equality (Q2871838) (← links)
- Imperative LF meta-programming (Q2871844) (← links)
- A list-machine benchmark for mechanized metatheory (extended abstract) (Q2871863) (← links)
- Encoding functional relations in Scunak (Q2871865) (← links)
- A bidirectional refinement type system for LF (Q2871879) (← links)
- A synthesis of the procedural and declarative styles of interactive theorem proving (Q2881098) (← links)
- Realizing the dependently typed \(\lambda\)-calculus (Q2883111) (← links)
- Towards Logical Frameworks in the Heterogeneous Tool Set Hets (Q2890328) (← links)
- GMeta: A Generic Formal Metatheory Framework for First-Order Representations (Q2892744) (← links)
- Extending MKM Formats at the Statement Level (Q2907314) (← links)
- A language-based approach to functionally correct imperative programming (Q2936790) (← links)
- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax (Q2938052) (← links)
- Higher-order term indexing using substitution trees (Q2946592) (← links)
- Mechanizing the metatheory of LF (Q2946633) (← links)
- Logical relations for a logical framework (Q2946721) (← links)
- Structural Focalization (Q2946730) (← links)
- Disjoint intersection types (Q2985786) (← links)
- Extensible Datasort Refinements (Q2988653) (← links)
- Programs Using Syntax with First-Class Binders (Q2988654) (← links)
- LINCX: A Linear Logical Framework with First-Class Contexts (Q2988658) (← links)
- Higher-Order Dynamic Pattern Unification for Dependent Types and Records (Q3007654) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- Lem: A Lightweight Tool for Heavyweight Semantics (Q3088021) (← links)
- Mechanizing the Metatheory of mini-XQuery (Q3100214) (← links)
- Implementing Cantor’s Paradise (Q3179294) (← links)
- Constraint solving in non-permutative nominal abstract syntax (Q3224672) (← links)
- A treatment of higher-order features in logic programming (Q3370572) (← links)
- Ruler: Programming Type Rules (Q3434622) (← links)
- Generic Literals (Q3453109) (← links)
- Formal Logic Definitions for Interchange Languages (Q3453113) (← links)
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← links)
- Inductive Beluga: Programming Proofs (Q3454100) (← links)
- There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners (Q3460064) (← links)
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory (Q3521979) (← links)
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF (Q3523179) (← links)
- The Abella Interactive Theorem Prover (System Description) (Q3541698) (← links)
- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description) (Q3541713) (← links)
- A Coverage Checking Algorithm for LF (Q3559763) (← links)
- Towards MKM in the Large: Modular Representation and Scalable Software Architecture (Q3582723) (← links)
- Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory (Q3612432) (← links)
