Zobrazeno 1 - 8
of 8
pro vyhledávání: '"Rouhling, Damien"'
Autor:
Rouhling, Damien, Farooque, Mahfuza, Graham-Lengrand, Stéphane, Mahboubi, Assia, Notin, Jean-Marc
Goal-directed proof search in first-order logic uses meta-variables to delay the choice of witnesses; substitutions for such variables are produced when closing proof-tree branches, using first-order unification or a theory-specific background reason
Externí odkaz:
http://arxiv.org/abs/1412.6790
Publikováno v:
ARRAY 2023-Workshop-PLDI 2023
ARRAY 2023-Workshop-PLDI 2023, Jun 2023, Orlando (Florida), United States.
ARRAY 2023-Workshop-PLDI 2023, Jun 2023, Orlando (Florida), United States.
International audience; We present OptiTrust, an interactive framework for optimizing general-purpose C code via series of programmer-guided, source-to-source transformations. Optimization steps are described in transformation scripts, expressed as O
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od_______165::e017aa96028b49fa00948376346d9fcd
https://inria.hal.science/hal-04053772/document
https://inria.hal.science/hal-04053772/document
Autor:
Affeldt, Reynald, Cohen, Cyril, Kerjean, Marie, Mahboubi, Assia, Rouhling, Damien, Sakaguchi, Kazuhiko
Publikováno v:
Automated Reasoning
This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topology and norms, in dependent type theory. This hierarchy is the backbone of a new library of formalized classical anal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=pmc_________::664bfd2ba25b8139bfc0a322a7c947df
http://europepmc.org/articles/PMC7324078
http://europepmc.org/articles/PMC7324078
Autor:
Affeldt, Reynald, Cohen, Cyril, Kerjean, Marie, Mahboubi, Assia, Rouhling, Damien, Sakaguchi, Kazuhiko
This paper discusses the design of a hierarchy of structures which combine linear algebra with concepts related to limits, like topol-ogy and norms, in dependent type theory. This hierarchy is the backbone of a new library of formalized classical ana
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=od______3393::d3e23938934c9afaea531a9e13a245e2
https://hal.inria.fr/hal-02463336
https://hal.inria.fr/hal-02463336
Autor:
Rouhling, Damien
Publikováno v:
Logic in Computer Science [cs.LO]. Université Côte d'Azur, 2019. English. ⟨NNT : 2019AZUR4058⟩
In this thesis, we put a library for analysis in the Coq proof assistant to the test through a case study in control theory. We formalise a proof of stability for the inverted pendulum, a standard example in control theory. Controlling the inverted p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::ff0323a2dce72f500ec390a2ad05f6a3
https://tel.archives-ouvertes.fr/tel-02333396
https://tel.archives-ouvertes.fr/tel-02333396
Autor:
Cohen, Cyril, Rouhling, Damien
Publikováno v:
JFLA 2017-Vingt-huitième Journées Francophones des Langages Applicatifs
JFLA 2017-Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
JFLA 2017-Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
National audience; Large scale reflection tactics are often implemented with ad-hoc data-structures and in a way which is specific to the problematic. This makes it hard to add improvements and to implement variations without writing an extensive the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::47d8e7230e6cbee4ea86a595a0049433
https://hal.inria.fr/hal-01414881
https://hal.inria.fr/hal-01414881
Publikováno v:
Journal of Formalized Reasoning
Journal of Formalized Reasoning, ASDD-AlmaDL, 2018
Journal of Formalized Reasoning, Vol 11, Iss 1, Pp 43-76 (2018)
Journal of Formalized Reasoning, 2018
Journal of Formalized Reasoning, ASDD-AlmaDL, 2018
Journal of Formalized Reasoning, Vol 11, Iss 1, Pp 43-76 (2018)
Journal of Formalized Reasoning, 2018
Formalizing analysis on a computer involves a lot of “epsilon-delta” reasoning, while informal reasoning may use some asymptotical hand-waving. Whether or not the arithmetic details are hidden using some abstraction like filters, a human user eve
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2b905ecf85847d6574b91d4fb0a57386
https://hal.inria.fr/hal-01719918
https://hal.inria.fr/hal-01719918
Autor:
Rouhling, Damien, Farooque, Mahfuza, Graham-Lengrand, Stéphane, Mahboubi, Assia, Notin, Jean-Marc
Publikováno v:
Cooperative Design, Visualization & Engineering: 12th International Conference, CDVE 2015, Mallorca, Spain, September 20-23, 2015, Proceedings; 2015, p220-236, 17p