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

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

1 2 3 4 5 next

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

1 2 3 4 5 next