Twelf
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Coq
- HYBRID
- ILTP
- Isabelle
- Ott
- metalib
- lang-n-play
- Cubical Agda
- Harpoon
- TALP
- TPS
- ML
- A linear logical framework
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
- Beluga
- lolliCoP
- HiLog
- THF0
- MetaPRL
- A semantic framework for proof evidence
- Canonical HybridLF: extending Hybrid with dependent types
- ETPS
- Automated techniques for provably safe mobile code.
- Prolog
- Nuprl
- Zenon
- Hets
- Automath
- MMT
- QMT
- OMDoc
- TNTBase
- Plastic
- 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
- MontiCore
- STEXIDE
- A formalized general theory of syntax with bindings: extended version
- \(\mathrm{HO}\pi\) in Coq
- On the effectiveness of higher-order logic programming in language-oriented programming
- Isabelle's metalogic: formalization and proof checker
- Harpoon: mechanizing metatheory interactively
- ALF
- FreshML
- Rensets and renaming-based recursion for syntax with bindings
- A formalization and proof checker for Isabelle's metalogic
- Functions-as-constructors higher-order unification: extended pattern unification
- Lem
- Tac
- Bedwyr
- Abella
- gaia
- LEGO
- Cayenne
- Epigram
- Agda
- DyC
- K tool
- Minlog
- System F in Agda, for fun and profit
- PLT Redex
- leanTAP
- aleanTAP
- PoplMark
- Gmeta
- LNgen
- Semantics of Mizar as an Isabelle object logic
- Mechanized metatheory revisited
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Imogen
- Mechanizing metatheory without typing contexts
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- A canonical locally named representation of binding
- A two-level logic approach to reasoning about computations
- Nominal Isabelle
- FoCaLiZe
- Vellvm
- Aglet
- LeoPARD
- MicroRogue
- TCB
- dedukti
- Proof checking and logic programming
- The future of logic: foundation-independence
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- scientific article; zbMATH DE number 1614684 (Why is no real title available?)
- CoALP
- Visible type application
- Automatically splitting a two-stage lambda calculus
- 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
- Developing (meta)theory of -calculus in the theory of contexts
- A representation of \(F_{\omega}\) in LF
- A third-order representation of the -calculus
- Producing proofs from an arithmetic decision procedure in elliptical LF
- A hybrid encoding of Howe's method for establishing congruence of bisimilarity
This page was built for software: Twelf
