Zobrazeno 1 - 9
of 9
pro vyhledávání: '"Thiré, François"'
Autor:
Dowek, Gilles, Thiré, François
Libraries of formal proofs are an important part of our mathematical heritage, but their usability and sustainability is poor. Indeed, each library is specific to a proof system, sometimes even to some version of this system. Thus, a library develope
Externí odkaz:
http://arxiv.org/abs/2305.00064
Publikováno v:
Logical Methods in Computer Science, Volume 19, Issue 1 (February 14, 2023) lmcs:8637
The lambda-Pi-calculus modulo theory is a logical framework in which many type systems can be expressed as theories. We present such a theory, the theory U, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory
Externí odkaz:
http://arxiv.org/abs/2111.00543
Autor:
Thiré, François
Publikováno v:
EPTCS 274, 2018, pp. 57-71
We observe today a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to co-operate because they do not implement
Externí odkaz:
http://arxiv.org/abs/1807.01873
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:
FSCD 2021-6th International Conference on Formal Structures for Computation and Deduction
FSCD 2021-6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires / Virtual, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.20⟩
FSCD 2021-6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires / Virtual, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.20⟩
The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4af361cf065543a6127b65cd8c3995c4
https://hal.inria.fr/hal-03279749
https://hal.inria.fr/hal-03279749
Autor:
Thiré, François
Publikováno v:
Computer Science [cs]. ENS Paris-Saclay, 2020. English
Logic in Computer Science [cs.LO]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG053⟩
Programming Languages [cs.PL]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG053⟩
Computer Science [cs]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG053⟩
Logic in Computer Science [cs.LO]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG053⟩
Programming Languages [cs.PL]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG053⟩
Computer Science [cs]. Université Paris-Saclay, 2020. English. ⟨NNT : 2020UPASG053⟩
There is today a large family of proof systems based upon variouslogics: The Calculus of Inductive Constructions, Higher-Order logic orSet theory, etc. The diversity of proof systems has the negativeconsequence that theorems are formalized many times
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::2ba7f54a23b25c4596a2b3c6565b1860
https://hal.archives-ouvertes.fr/tel-03224039
https://hal.archives-ouvertes.fr/tel-03224039
Autor:
Thiré, François
Today, we observe a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to cooperate because they do not implement
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::6c7f972d62fd7937816241e290e49c21
https://hal.inria.fr/hal-01668250/document
https://hal.inria.fr/hal-01668250/document
Publikováno v:
International School On Rewriting 2017
International School On Rewriting 2017, Jul 2017, Eindhoven, Netherlands
International School On Rewriting 2017, Jul 2017, Eindhoven, Netherlands
International audience
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::d13d548dd0df5a3a358f19e911a2de1a
https://inria.hal.science/hal-01668246/document
https://inria.hal.science/hal-01668246/document
Autor:
Thiré, François
Publikováno v:
Computer Science [cs]. 2016
International audience; dedukti is a logical framework that implements the λΠ− modulo theory, an extension of the simply typed lambda calculus with dependent types and rewriting rules. It aims to be a back-end for other proof checkers by compilin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::73352118f7edc14008dfbb1d14706ee6
https://hal.inria.fr/hal-01424816/document
https://hal.inria.fr/hal-01424816/document