Zobrazeno 1 - 10
of 25
pro vyhledávání: '"Kahn, Gilles"'
Autor:
Kahn, Gilles
Publikováno v:
Interstices
Interstices, INRIA, 2004
Interstices, 2004
Interstices, INRIA, 2004
Interstices, 2004
National audience; Cet exposé de Gilles Kahn, donné le 30 mars 2004 à l’Académie des sciences, présente l’articulation entre ce qu’il est facile de percevoir : les technologies et ce qui est souvent moins bien compris : la science.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::0cc854bfaad32bb8c2220f60f06c66b5
https://hal.inria.fr/hal-01350279
https://hal.inria.fr/hal-01350279
Publikováno v:
[Research Report] RT-0256, INRIA. 2002, pp.46
Projet COQ; Coq is a proof assistant based on a higher-order logic. Coq allows to handle calculus mathematical assertions and to check mechanically proofs of these assertions. It helps to find formal proofs, and allows extraction of a certified progr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::99d6525c5a9aedd3dc866cf4337f9574
https://inria.hal.science/inria-00069918/document
https://inria.hal.science/inria-00069918/document
Publikováno v:
[Research Report] RT-0204, INRIA. 1997, pp.44
Projet COQ; Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. This document is a tutorial for the version V6.1 of Coq. This version is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::366cab458c56748bfe2ebac415fe4117
https://inria.hal.science/inria-00069967
https://inria.hal.science/inria-00069967
Publikováno v:
RT-0178, INRIA. 1995, pp.46
Projet COQ
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::781d3ffd597690bf152f141f1002e794
https://hal.inria.fr/inria-00069993/document
https://hal.inria.fr/inria-00069993/document
Publikováno v:
RR-2459, INRIA. 1995
In this paper, we propose a method for presenting formal proofs in an intelligible form. We describe a transducer from proof objects ($\lambda$-terms in the Calculus of Constructions) to pseudo natural language that has been implemented for the Coq s
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______165::e60e9f4cbc8ac2fd827070a303af4bdf
https://inria.hal.science/inria-00074217/file/RR-2459.pdf
https://inria.hal.science/inria-00074217/file/RR-2459.pdf
Publikováno v:
Proceedings of the Fifth ACM SIGSOFT Symposium: Software Development Environments; Dec1992, p120-129, 10p
Publikováno v:
Proceedings of the 1986 ACM Conference: LISP & Functional Programming; 8/ 8/1986, p13-27, 15p