Zobrazeno 1 - 4
of 4
pro vyhledávání: '"Crance, Enzo"'
Libraries of formalized mathematics use a possibly broad range of different representations for a same mathematical concept. Yet light to major manual input from users remains most often required for obtaining the corresponding variants of theorems,
Externí odkaz:
http://arxiv.org/abs/2310.14022
Autor:
Blot, Valentin, Cousineau, Denis, Crance, Enzo, de Prisque, Louise Dubois, Keller, Chantal, Mahboubi, Assia, Vial, Pierre
Publikováno v:
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '23), January 16-17, 2023, Boston, MA, USA
In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This ve
Externí odkaz:
http://arxiv.org/abs/2204.02643
Autor:
Blot, Valentin, Cousineau, Denis, Crance, Enzo, de Prisque, Louise Dubois, Keller, Chantal, Mahboubi, Assia, Vial, Pierre
Publikováno v:
CPP 2023-Certified Programs and Proofs
CPP 2023-Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩
CPP 2023-Certified Programs and Proofs, Jan 2023, Boston, United States. pp.1-15, ⟨10.1145/3573105.3575676⟩
International audience; In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected l
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fe662381e483c147d8f9996499b886e3
https://inria.hal.science/hal-03901019v2/document
https://inria.hal.science/hal-03901019v2/document
Publikováno v:
Journées Francophones des Langages Applicatifs
JFLA 2022-33èmes Journées Francophones des Langages Applicatifs
JFLA 2022-33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.261-263
JFLA 2022-33èmes Journées Francophones des Langages Applicatifs
JFLA 2022-33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.261-263
National audience; Dans un assistant de preuve comme Coq, un même objet mathématique peut souvent être formalisé par différentes structures de données. Par exemple, le type Z des entiers binaires, dans la bibliothèque standard de Coq, représe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::8b57ede547ba52742782865ff2d18861
https://hal.inria.fr/hal-03626851
https://hal.inria.fr/hal-03626851