Dependent types and HOL
Dependent Types
Preuve formelle assistée par ordinateur (LMFI)
TD8: Définitions inductives de prédicats
Page du cours
HOL
Symmetry in HOL
TD9: Enigme de MU: Définitions inductives de prédicats et analyse par cas
TD9 : Définitions inductives de prédicats et analyse par cas
Isabelle
Isabelle (named by Lawrence Paulson after the daughter of Gérard Huet, as a tribute): a popular generic theorem prover
TD10: Damier (checker)
NB: Boards are finite. Number of configurations:
[Final Coq Project] Coherence of Heyting’s arithmetic
Coherence of Heyting’s arithmetic in Coq