Twelf
Twelf is a language used to specify, implement, and prove properties of deductive systems such as programming languages and logics. Large research projects using Twelf include the TALT typed assembly language, a foundational proof-carrying-code system, and a type safety proof for Standard ML.
Keywords for this software
References in zbMATH (referenced in 169 articles , 2 standard articles )
Showing results 1 to 20 of 169.
Sorted by year (- Bry, François: In praise of impredicativity: a contribution to the formalization of meta-programming (2020)
- Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
- Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
- Mahmoud, Mohamed Yousri; Felty, Amy P.: Formalization of metatheory of the quipper quantum programming language in a linear logic (2019)
- Miller, Dale: Mechanized metatheory Revisited (2019)
- Momigliano, Alberto; Pientka, Brigitte; Thibodeau, David: A case study in programming coinductive proofs: Howe’s method (2019)
- Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
- Chihani, Zakaria; Miller, Dale; Renaud, Fabien: A semantic framework for proof evidence (2017)
- Dunfield, Joshua: Extensible datasort refinements (2017)
- Ferreira, Francisco; Pientka, Brigitte: Programs using syntax with first-class binders (2017)
- Georges, Aina Linn; Murawska, Agata; Otis, Shawn; Pientka, Brigitte: \textscLincx: a linear logical framework with first-class contexts (2017)
- Honsell, Furio; Liquori, Luigi; Maksimovic, Petar; Scagnetto, Ivan: (\mathsfLLF_\mathcalP): a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads (2017)
- Kaiser, Jonas; Pientka, Brigitte; Smolka, Gert: Relating system F and (\lambda2): a case study in Coq, Abella and Beluga (2017)
- Kaliszyk, Cezary; Pąk, Karol: Presentation and manipulation of Mizar properties in an Isabelle object logic (2017)
- Kammar, Ohad; Pretnar, Matija: No value restriction is needed for algebraic effects and handlers (2017)
- Miller, Dale: Proof checking and logic programming (2017)
- Stump, Aaron: The calculus of dependent lambda eliminations (2017)
- Crole, Roy L.; Furniss, Amy: Canonical HybridLF: extending Hybrid with dependent types (2016)
- Eisenberg, Richard A.; Weirich, Stephanie; Ahmed, Hamidhasan G.: Visible type application (2016)
- Feltman, Nicolas; Angiuli, Carlo; Acar, Umut A.; Fatahalian, Kayvon: Automatically splitting a two-stage lambda calculus (2016)