• Coq

  • Referenced in 1898 articles [sw00161]
  • Coq is a formal proof management system. It...
  • ML

  • Referenced in 522 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • Beluga

  • Referenced in 26 articles [sw01321]
  • Our main interest in this project is to...
  • Irdis

  • Referenced in 22 articles [sw09690]
  • Irdis: a language with dependent types. Idris is...
  • CompCert

  • Referenced in 50 articles [sw09737]
  • The CompCert project investigates the formal verification of...
  • TCB

  • Referenced in 5 articles [sw13591]
  • A trustworthy proof checker. Proof-Carrying Code (PCC...
  • Idris

  • Referenced in 37 articles [sw20011]
  • Idris is a general purpose pure functional programming...
  • ELPI

  • Referenced in 9 articles [sw28521]
  • ELPI: Fast, Embeddable, λProlog Interpreter. We present a...