Zobrazeno 1 - 10
of 19
pro vyhledávání: '"Barras, Bruno"'
Autor:
Barras, Bruno, Maestracci, Valentin
Publikováno v:
EPTCS 332, 2021, pp. 54-67
In this paper, we make a substantial step towards an encoding of Cubical Type Theory (CTT) in the Dedukti logical framework. Type-checking CTT expressions features a decision procedure in a de Morgan algebra that so far could not be expressed by the
Externí odkaz:
http://arxiv.org/abs/2101.03810
The work described in this paper improves the reactivity of the Coq system by completely redesigning the way it processes a formal document. By subdividing such work into independent tasks the system can give precedence to the ones of immediate inter
Externí odkaz:
http://arxiv.org/abs/1506.05605
Autor:
Barras, Bruno, Huesca, Lourdes del Carmen González, Herbelin, Hugo, Régis-Gianas, Yann, Tassi, Enrico, Wenzel, Makarius, Wolff, Burkhart
This is an overview of the Paral-ITP project, which intents to make the proof assistants Isabelle and Coq fit for the multicore era.
Comment: Conferences on Intelligent Computer Mathematics CICM 2013. The final publication is available at http:/
Comment: Conferences on Intelligent Computer Mathematics CICM 2013. The final publication is available at http:/
Externí odkaz:
http://arxiv.org/abs/1305.7360
Autor:
Wang, Qian, Barras, Bruno
Publikováno v:
Computer Science Logic 2013
Computer Science Logic 2013, Aug 2013, Dagstuhl, Germany. pp.653--667, ⟨10.4230/LIPIcs.CSL.2013.653⟩
Computer Science Logic 2013, Aug 2013, Dagstuhl, Germany. pp.653--667, ⟨10.4230/LIPIcs.CSL.2013.653⟩
International audience; Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions (CC) provides with stronger type-checking capabilities and makes the proof development closer to intuition. Sinc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7018f6762d3ac85059931837c2532d2d
https://hal.inria.fr/hal-00937197
https://hal.inria.fr/hal-00937197
Autor:
Aczel, Peter, Ahrens, Benedikt, Altenkirch, Thorsten, Awodey, Steve, Barras, Bruno, Bauer, Andrej, Bertot, Yves, Bezem, Marc, Coquand, Thierry, Finster, Eric, Grayson, Daniel, Herbelin, Hugo, Joyal, André, Licata, Dan, Lumsdaine, Peter, Mahboubi, Assia, Martin-Löf, Per, Melikhov, Sergey, Pelayo, Alvaro, Polonsky, Andrew, Shulman, Michael, Sozeau, Matthieu, Spitters, Bas, Van Den Berg, Benno, Voevodsky, Vladimir, Warren, Michael, Angiuli, Carlo, Bordg, Anthony, Brunerie, Guillaume, Kapulkin, Chris, Rijke, Egbert, Sojakova, Kristina, Avigad, Jeremy, Cohen, Cyril, Constable, Robert, Curien, Pierre-Louis, Dybjer, Peter, Escardó, Martín, Hou, Kuen-Bang, Gambino, Nicola, Garner, Richard, Gonthier, Georges, Hales, Thomas, Harper, Robert, Hofmann, Martin, Hofstra, Pieter, Koch, Joachim, Kraus, Nicolai, Li, Nuo, Luo, Zhaohui, Nahas, Michael, Palmgren, Erik, Riehl, Emily, Scott, Dana, Scott, Philip, Soloviev, Sergei
Publikováno v:
Aucun, pp.448, 2013
International audience; Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy the- ory and type theory. Homotopy the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::de92f76e2e2cdba2edecab5b46a276a0
https://inria.hal.science/hal-00935057
https://inria.hal.science/hal-00935057
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Publikováno v:
Journal of Cryptographic Engineering; Apr2017, Vol. 7 Issue 1, p75-85, 11p
Autor:
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, Herbelin, Hugo, Huet, Gérard, Muñoz, César, Murthy, Chetan, Parent, Catherine, Paulin-Mohring, Christine, Saïbi, Amokrane, Werner, Benjamin
Publikováno v:
[Research Report] RT-0203, INRIA. 1997, pp.214
Projet COQ; Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and ftp.ens-lyon.fr:/pub/LIP/COQ/V6.1
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::2ecf7fa50804c06ea1f61a3e0a318729
https://inria.hal.science/inria-00069968/file/RT-0203.pdf
https://inria.hal.science/inria-00069968/file/RT-0203.pdf
Autor:
Barras, Bruno
Publikováno v:
[Research Report] RR-3026, INRIA. 1996
Projet COQ; The essential step of the formal verification of a proof-checker such as Coq is the verification of its kernel: a type-checker for the Calculus of Inductive Constructions (CIC) which is its underlying formalism. The present work is a firs
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______165::f94a4ddda11950a99a45eed3b9cb8ccf
https://inria.hal.science/inria-00073667
https://inria.hal.science/inria-00073667
Publikováno v:
Types for Proofs & Programs (9783642024436); 2009, p32-48, 17p