Zobrazeno 1 - 3
of 3
pro vyhledávání: '"de Prisque, Louise Dubois"'
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
Publikováno v:
EPTCS 336, 2021, pp. 24-39
Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further away from fi
Externí odkaz:
http://arxiv.org/abs/2107.02353
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