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

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

1 2 3 4 5 6 next

  1. 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)
  2. Miller, Dale: Proof checking and logic programming (2017)
  3. Feltman, Nicolas; Angiuli, Carlo; Acar, Umut A.; Fatahalian, Kayvon: Automatically splitting a two-stage lambda calculus (2016)
  4. Oliveira, Bruno C.d.S.; Shi, Zhiyuan; Alpuim, João: Disjoint intersection types (2016)
  5. Rabe, Florian: The future of logic: foundation-independence (2016)
  6. Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
  7. Miller, Dale: Proof checking and logic programming (2015)
  8. Pientka, Brigitte; Cave, Andrew: Inductive Beluga: programming proofs (2015)
  9. Wisniewski, Max; Steen, Alexander; Benzmüller, Christoph: LeoPARD -- a generic platform for the implementation of higher-order reasoners (2015)
  10. Bauer, Andrej; Pretnar, Matija: An effect system for algebraic effects and handlers (2014)
  11. Constable, Robert; Bickford, Mark: Intuitionistic completeness of first-order logic (2014)
  12. Park, Jonghyun; Seo, Jeongbong; Park, Sungwoo; Lee, Gyesik: Mechanizing metatheory without typing contexts (2014)
  13. Geuvers, Herman; Nederpelt, Rob: N. G. de Bruijn’s contribution to the formalization of mathematics (2013)
  14. Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef: The Mizar Mathematical Library in OMDoc: translation and applications (2013)
  15. Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
  16. Miller, Dale; Pimentel, Elaine: A formal framework for specifying sequent calculus proof systems (2013)
  17. Rabe, Florian; Kohlhase, Michael: A scalable module system (2013)
  18. Rabe, Florian; Sojakova, Kristina: Logical relations for a logical framework (2013)
  19. Accattoli, Beniamino: Proof pearl: abella formalization of $\lambda $-calculus cube property (2012)
  20. Appel, Andrew W.; Dockins, Robert; Leroy, Xavier: A list-machine benchmark for mechanized metatheory (2012)

1 2 3 4 5 6 next