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

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

1 2 3 ... 5 6 7 next

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

1 2 3 ... 5 6 7 next