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.


References in zbMATH (referenced in 169 articles , 2 standard articles )

Showing results 1 to 20 of 169.
Sorted by year (citations)

1 2 3 ... 7 8 9 next

  1. Bry, François: In praise of impredicativity: a contribution to the formalization of meta-programming (2020)
  2. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  3. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
  4. Mahmoud, Mohamed Yousri; Felty, Amy P.: Formalization of metatheory of the quipper quantum programming language in a linear logic (2019)
  5. Miller, Dale: Mechanized metatheory Revisited (2019)
  6. Momigliano, Alberto; Pientka, Brigitte; Thibodeau, David: A case study in programming coinductive proofs: Howe’s method (2019)
  7. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  8. Chihani, Zakaria; Miller, Dale; Renaud, Fabien: A semantic framework for proof evidence (2017)
  9. Dunfield, Joshua: Extensible datasort refinements (2017)
  10. Ferreira, Francisco; Pientka, Brigitte: Programs using syntax with first-class binders (2017)
  11. Georges, Aina Linn; Murawska, Agata; Otis, Shawn; Pientka, Brigitte: \textscLincx: a linear logical framework with first-class contexts (2017)
  12. 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)
  13. Kaiser, Jonas; Pientka, Brigitte; Smolka, Gert: Relating system F and (\lambda2): a case study in Coq, Abella and Beluga (2017)
  14. Kaliszyk, Cezary; Pąk, Karol: Presentation and manipulation of Mizar properties in an Isabelle object logic (2017)
  15. Kammar, Ohad; Pretnar, Matija: No value restriction is needed for algebraic effects and handlers (2017)
  16. Miller, Dale: Proof checking and logic programming (2017)
  17. Stump, Aaron: The calculus of dependent lambda eliminations (2017)
  18. Crole, Roy L.; Furniss, Amy: Canonical HybridLF: extending Hybrid with dependent types (2016)
  19. Eisenberg, Richard A.; Weirich, Stephanie; Ahmed, Hamidhasan G.: Visible type application (2016)
  20. Feltman, Nicolas; Angiuli, Carlo; Acar, Umut A.; Fatahalian, Kayvon: Automatically splitting a two-stage lambda calculus (2016)

1 2 3 ... 7 8 9 next