A Coinductive Approach to Proof Search

Autor: José Espírito Santo, Ralph Matthes, Luís Pinto

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 126, Iss Proc. FICS 2013, Pp 28-43 (2013)

We propose to study proof search from a coinductive point of view. In this paper, we consider intuitionistic logic and a focused system based on Herbelin's LJT for the implicational fragment. We introduce a variant of lambda calculus with potentially

Externí odkaz: https://doaj.org/article/397a4c98dcdd42d28b3daf73fcedef9c

Implementing a Category-Theoretic Framework for Typed Abstract Syntax

Autor: Benedikt Ahrens, Ralph Matthes, Anders Mörtberg

Publikováno v: CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP 2022
(à paraître) Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’22)
11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022)
11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), Jan 2022, Philadelphia, PA, United States. ⟨10.1145/3497775.3503678⟩

Accepted to CPP 2022; International audience; In previous work (“From signatures to monads in UniMath”), we described a category-theoretic construction of abstract syntax from a signature, mechanized in the UniMath library based on the Coq proof

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8fca1362af037f15d322ea13ad149b4a
http://arxiv.org/abs/2112.06984

From signatures to monads in UniMath

Autor: Benedikt Ahrens, Anders Mörtberg, Ralph Matthes

Publikováno v: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2019, 63 (2), pp.285-318. ⟨10.1007/s10817-018-9474-4⟩
Journal of Automated Reasoning, 2019, 63 (2), pp.285-318. ⟨10.1007/s10817-018-9474-4⟩

The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::220aa7e233cc7cde3e930c3bf3c004b0
https://hal.inria.fr/hal-01410487

Decidability of several concepts of finiteness for simple types

Autor: Luís Pinto, José Espírito Santo, Ralph Matthes

Publikováno v: Fundamenta Informaticae
Fundamenta Informaticae, IOS Press, 2019, 170 (1-3), pp.111-138. ⟨10.3233/FI-2019-1857⟩
Repositório Científico de Acesso Aberto de Portugal
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP
Fundamenta Informaticae, 2019, 170 (1-3), pp.111-138. ⟨10.3233/FI-2019-1857⟩

If we consider as "member" of a simple type the outcome of any successful (possibly infinite) run of bottom-up proof search that starts from the type, then several concepts of "finiteness" for simple types are possible: the finiteness of the search s

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::87f3cefbefa14a900fc0361e6b2331d9
https://hal.archives-ouvertes.fr/hal-02119503

A Coinductive Approach to Proof Search through Typed Lambda-Calculi

Autor: Luís Pinto, José Espírito Santo, Ralph Matthes

Publikováno v: Annals of Pure and Applied Logic
Annals of Pure and Applied Logic, Elsevier Masson, 2021, 172 (10), ⟨10.1016/j.apal.2021.103026⟩
Annals of Pure and Applied Logic, 2021, 172 (10), ⟨10.1016/j.apal.2021.103026⟩
Repositório Científico de Acesso Aberto de Portugal
Repositório Científico de Acesso Aberto de Portugal (RCAAP)
instacron:RCAAP

In reductive proof search, proofs are naturally generalized by solutions, comprising all (possibly infinite) structures generated by locally correct, bottom-up application of inference rules. We propose a rather natural extension of the Curry-Howard

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::48c51021f018f6544bc396de417d7135
http://arxiv.org/abs/1602.04382