Theorem proving and provers for reliable theory and implementations
Coq Agda OCaml Isabelle Standard ML
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
AdamChlipala
CyrilCohen
DaisukeSato
FadouaGhourabi
JacquesGarrigue
KazuhikoSakaguchi
KazuhisaNakasho
KeiTsujimoto
KeishiSuda
MasahiroSakai
MasahiroSato
MitsuharuYamamoto
SosukeMoriguchi
TakashiMiyamoto
YoichiHirai
README.md

README.md

TPP2014

Theorem proving and provers for reliable theory and implementations

Problem (pdf)

Authors Wiki

  • Adam Chlipala (Coq)
  • Cyri Cohen (Ssreflect)
  • Daisuke Sato (Coq)
  • Fadoua Ghourabi (Isabelle/HOL)
  • Jacques Garrigues (Coq)
  • Kazuhiko Sakaguchi (Ssreflect)
  • Kazuhisa Nakasho (Mizar)
  • Kei Tsujimoto (HOL Light)
  • Keishi Suda (Ssreflect)
  • Masahiko Sakai (Agda)
  • Masahiro Sato (Coq)
  • Mitsuharu Yamamoto (Ssreflect, HOL4)
  • Sosuke Moriguchi (Coq)
  • Takashi Miyamoto (Coq)
  • Yoichi Hirai (Ssreflect)

Public Repository since 2014/11/19.

TPP2014 workshop HP: http://imi.kyushu-u.ac.jp/lasm/tpp2014/