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 140 articles , 2 standard articles )

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

1 2 3 ... 5 6 7 next

  1. Cheney, James; Momigliano, Alberto: $\alpha\mathrmCheck$: a mechanized metatheory model checker (2017)
  2. Chihani, Zakaria; Miller, Dale; Renaud, Fabien: A semantic framework for proof evidence (2017)
  3. Dunfield, Joshua: Extensible datasort refinements (2017)
  4. Ferreira, Francisco; Pientka, Brigitte: Programs using syntax with first-class binders (2017)
  5. Georges, Aina Linn; Murawska, Agata; Otis, Shawn; Pientka, Brigitte: Lincx: a linear logical framework with first-class contexts (2017)
  6. Honsell, Furio; Liquori, Luigi; Maksimovic, Petar; Scagnetto, Ivan: $\mathsfLLF_\CalP$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads (2017)
  7. Kaliszyk, Cezary; Pąk, Karol: Presentation and manipulation of Mizar properties in an Isabelle object logic (2017)
  8. Kammar, Ohad; Pretnar, Matija: No value restriction is needed for algebraic effects and handlers (2017)
  9. Miller, Dale: Proof checking and logic programming (2017)
  10. Stump, Aaron: The calculus of dependent lambda eliminations (2017)
  11. Eisenberg, Richard A.; Weirich, Stephanie; Ahmed, Hamidhasan G.: Visible type application (2016)
  12. Feltman, Nicolas; Angiuli, Carlo; Acar, Umut A.; Fatahalian, Kayvon: Automatically splitting a two-stage lambda calculus (2016)
  13. Honsell, Furio; Lenisa, Marina; Liquori, Luigi; Scagnetto, Ivan: Implementing Cantor’s paradise (2016)
  14. Oliveira, Bruno C.d.S.; Shi, Zhiyuan; Alpuim, João: Disjoint intersection types (2016)
  15. Rabe, Florian: The future of logic: foundation-independence (2016)
  16. Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
  17. Horozal, Fulya; Rabe, Florian: Formal logic definitions for interchange languages (2015)
  18. Miller, Dale: Proof checking and logic programming (2015)
  19. Pientka, Brigitte; Cave, Andrew: Inductive Beluga: programming proofs (2015)
  20. Rabe, Florian: Lax theory morphisms (2015)

1 2 3 ... 5 6 7 next