Zobrazeno 1 - 10
of 112
pro vyhledávání: '"BLANQUI, FRÉDÉRIC"'
Autor:
Felicissimo, Thiago, Blanqui, Frédéric
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 3 (September 10, 2024) lmcs:12213
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assi
Externí odkaz:
http://arxiv.org/abs/2308.15465
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assi
Externí odkaz:
http://arxiv.org/abs/2211.05700
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:
Hondet, Gabriel, Blanqui, Frédéric
The $\lambda$$\Pi$-calculus modulo theory is a logical framework in which various logics and type systems can be encoded, thus helping the cross-verification and interoperability of proof systems based on those logics and type systems. In this paper,
Externí odkaz:
http://arxiv.org/abs/2110.13704
Autor:
Blanqui, Frédéric
Publikováno v:
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Jun 2020, Paris, France. pp.14
The expressiveness of dependent type theory can be extended by identifying types modulo some additional computation rules. But, for preserving the decidability of type-checking or the logical consistency of the system, one must make sure that those u
Externí odkaz:
http://arxiv.org/abs/2010.16111
Autor:
Hondet, Gabriel, Blanqui, Frédéric
Publikováno v:
FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. pp.16
Dedukti is a type-checker for the $\lambda$$\Pi$-calculus modulo rewriting, an extension of Edinburgh's logicalframework LF where functions and type symbols can be defined by rewrite rules. It thereforecontains an engine for rewriting LF terms and ty
Externí odkaz:
http://arxiv.org/abs/2010.16115
Publikováno v:
EPTCS 301, 2019, pp. 27-35
Proof assistants often call automated theorem provers to prove subgoals. However, each prover has its own proof calculus and the proof traces that it produces often lack many details to build a complete proof. Hence these traces are hard to check and
Externí odkaz:
http://arxiv.org/abs/1908.09479
Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting sy
Externí odkaz:
http://arxiv.org/abs/1906.11649
Publikováno v:
16th International Workshop on Termination, Jul 2018, Oxford, United Kingdom
The Size-Change Termination principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a system of dependent types e
Externí odkaz:
http://arxiv.org/abs/1812.01853
Autor:
Blanqui, Frédéric, Reis, Giselle
Publikováno v:
EPTCS 274, 2018
This volume contains a selection of papers presented at LFMTP 2018, the 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held on July 7, 2018, in Oxford, UK. The workshop was affiliated with the 3rd i
Externí odkaz:
http://arxiv.org/abs/1807.01352