The following pages link to Twelf (Q18957):
Displayed 50 items.
- The future of logic: foundation-independence (Q263104) (← links)
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← links)
- A scalable module system (Q391632) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- Nominal abstraction (Q617715) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Verifying termination and reduction properties about higher-order logic programs (Q850496) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (Q865658) (← links)
- A linear logical framework (Q1400718) (← links)
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- Canonical HybridLF: extending Hybrid with dependent types (Q1744412) (← links)
- Automated techniques for provably safe mobile code. (Q1853627) (← links)
- A formal framework for specifying sequent calculus proof systems (Q1944778) (← links)
- The Mizar Mathematical Library in OMDoc: translation and applications (Q1945907) (← links)
- A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (Q1945915) (← links)
- A list-machine benchmark for mechanized metatheory (Q1945921) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- On the effectiveness of higher-order logic programming in language-oriented programming (Q2039939) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- Harpoon: mechanizing metatheory interactively (Q2055903) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- System F in Agda, for fun and profit (Q2176683) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Formalization of metatheory of the Quipper quantum programming language in a linear logic (Q2331074) (← links)
- Mechanizing metatheory without typing contexts (Q2352491) (← links)
- Presentation and manipulation of Mizar properties in an Isabelle object logic (Q2364678) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- Proof checking and logic programming (Q2628296) (← links)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (Q2655326) (← links)
- (Q2723406) (← links)
- Visible Type Application (Q2802481) (← links)
- Automatically Splitting a Two-Stage Lambda Calculus (Q2802484) (← links)
- On the Expressivity of Minimal Generic Quantification (Q2804937) (← links)
- Explicit Contexts in LF (Extended Abstract) (Q2804940) (← links)
- Case Analysis of Higher-Order Data (Q2804942) (← links)
- Reasoning in Abella about Structural Operational Semantics Specifications (Q2804943) (← links)
- Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. (Q2841233) (← links)
- A Representation of Fω in LF (Q2841235) (← links)
- A Third-Order Representation of the λμ-Calculus (Q2841236) (← links)