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

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

1 2 3 ... 5 6 7 next