, The Coq proof assistant
Parmenides 149a7-c3. a proof by complete induction? Archive for History of Exact Sciences, vol.55, pp.57-76, 2000. ,
Program evaluation research task, Summary report Phase 1 and 2, 1958. ,
, Prior Analytics, p.350
Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions, 2004. ,
CoLoR, a Coq Library on rewriting and termination, Workshop on Termination, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00084835
Logique, méthode pour l'informatique fondamentale. Hermes, 1991. a Formal and Constructive Equivalence ,
Topological sorting of large networks, Commun. ACM, vol.5, issue.11, pp.558-562, 1962. ,
The Art of Computer Programming, vol.1, 1973. ,
Topological ordering of a list of randomly-numbered elements of a network, Commun. ACM, vol.4, issue.4, pp.167-168, 1961. ,
Arithmeticorum libri duo, p.1575 ,
Automatic machine methods of testing pert networks for consistency, 1960. ,
, Studies in Logic and the Foundations of Mathematics. North-Holland, vol.133, 1994.
Arithmetices principia, nova methodo exposita, 1889. ,
Origins of the calculus of binary relations, Logic in Computer Science, 1992. ,
, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980.
Sur l'extension de l'ordre partiel, Fund. Math, 1930. ,
Constructivism in mathematics. An introduction, vol.1, 1988. ,
Zur Einfürung der transfiniten Zahlen, Acta Litterarum ac Scientiarum Regiae Universitatis Hungaricae Franscisco-Josephinae Section Scientiarum Mathematicarum, vol.1, pp.199-208, 1923. ,
, Principia Mathematica. Cambridge Mathematical Library, 1910.