Zobrazeno 1 - 10
of 24
pro vyhledávání: '"Guidi, Ferruccio"'
Autor:
Guidi, Ferruccio <1969>
In this thesis, the author presents a query language for an RDF (Resource Description Framework) database and discusses its applications in the context of the HELM project (the Hypertextual Electronic Library of Mathematics). This language aims at me
Externí odkaz:
http://amsdottorato.unibo.it/7197/
Autor:
Guidi, Ferruccio
We advocate the use of de Bruijn's universal abstraction $\lambda^\infty$ for the quantification of schematic variables in the predicative setting and we present a typed $\lambda$-calculus featuring the quantifier $\lambda^\infty$ accompanied by othe
Externí odkaz:
http://arxiv.org/abs/1911.12749
Autor:
Guidi, Ferruccio
The formal system $\lambda\delta$ is a typed lambda calculus derived from $\Lambda_\infty$, aiming to support the foundations of Mathematics that require an underlying theory of expressions (for example the Minimal Type Theory). The system is develop
Externí odkaz:
http://arxiv.org/abs/1411.0154
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.
Autor:
Guidi, Ferruccio
Publikováno v:
Journal of Formalized Reasoning, Vol 8, Iss 1, Pp 93-116 (2016)
Landau's "Grundlagen der Analysis" formalized in the language Aut-QE, represents an early milestone in computer-checked mathematics and is the only non-trivial development finalized in the languages of the Automath family. Here we discuss an implemen
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::165b6c4a85111afbdb6fec880cb95568
https://jfr.unibo.it/article/view/4716
https://jfr.unibo.it/article/view/4716
Autor:
Guidi, Ferruccio
Publikováno v:
Guidi, Ferruccio (2017) The Formal System \lambda \Upsilon P. [Preprint]
We propose to extend the Edinburgh Logical Framework with Automath's unified abstraction.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d765a2f7f7fbbdab451b73e61313c451
http://amsacta.unibo.it/5754/
http://amsacta.unibo.it/5754/
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:
LNCS
Proceedings of LPAR
Proceedings of LPAR, Nov 2015, Suva, Fiji
Proceedings of LPAR
Proceedings of LPAR, Nov 2015, Suva, Fiji
International audience; We present a new interpreter for λProlog that runs consistently faster than the byte code compiled by Teyjus, that is believed to be the best available implementation of λProlog. The key insight is the identification of a fr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::dedbe8c9a40bd2a2fb2740cb6a8797ff
https://hal.inria.fr/hal-01176856
https://hal.inria.fr/hal-01176856
We present a formalization of pure ?-calculus for the Matita interactive theorem prover, including the proofs of two relevant results in reduction theory: the confluence theorem and the standardization theorem. The proof of the latter is based on a n
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::bb75d23f2b1fcac7c09158fe7f70b74f
Publikováno v:
Mathematics in Computer Science; Dec2016, Vol. 10 Issue 4, p409-427, 19p