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

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

1 2 3 4 5 next

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

1 2 3 4 5 next