• Coq

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

  • Referenced in 604 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • ML

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

  • Referenced in 840 articles [sw03521]
  • Haskell is a standardized, general-purpose purely functional...
  • Miranda

  • Referenced in 150 articles [sw04986]
  • Miranda: A non-strict functional language with polymorphic...
  • Nuprl

  • Referenced in 387 articles [sw06751]
  • The Nuprl system is a framework for reasoning...
  • Twelf

  • Referenced in 169 articles [sw06888]
  • Twelf is a language used to specify, implement...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • LEGO is an interactive proof development system (proof...
  • Cayenne

  • Referenced in 29 articles [sw09686]
  • Cayenne — a language with dependent types. Cayenne is...
  • Epigram

  • Referenced in 22 articles [sw09687]
  • Epigram: Practical programming with dependent types. Find the...
  • Paco

  • Referenced in 17 articles [sw10885]
  • Paco: A Coq Library for Parameterized Coinduction. Paco...
  • llprover

  • Referenced in 4 articles [sw11993]
  • A Linear Logic Prover (llprover). This small program...
  • PELCR

  • Referenced in 4 articles [sw20841]
  • PELCR, parallel environment for optimal lambda-calculus reduction...
  • ALGOL 60

  • Referenced in 502 articles [sw21807]
  • ALGOL 60 (short for Algorithmic Language 1960) is...
  • MiniML

  • Referenced in 46 articles [sw29625]
  • A modal analysis of staged computation. We show...
  • Zsyntax

  • Referenced in 2 articles [sw30123]
  • Zsyntax: A Formal Language for Molecular Biology with...