Zobrazeno 1 - 10
of 17
pro vyhledávání: '"Álvaro Tasistro"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 27-41 (2018)
We present a full formalization in Martin-Löf's Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using first-order syntax with one sort of names for both free and bound variables and Stoughton's multiple substitution.
Externí odkaz:
https://doaj.org/article/c161cb7a049e4a60b46dd04cfe548233
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 11-26 (2018)
We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then define a generic alpha-equivalence relation over the types of the uni
Externí odkaz:
https://doaj.org/article/fa5114a1eeab49e8a7ee3d22bb0b8bb3
Publikováno v:
Mathematical Structures in Computer Science. 31:341-360
AbstarctWe formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::985ac2b22eacd513cd83249570e60a18
https://doi.org/10.1017/s0960129521000335
https://doi.org/10.1017/s0960129521000335
Publikováno v:
LSFA
We consider a pre-existing formalization in Constructive Type Theory of the pure Lambda Calculus in its presentation in first order syntax with only one sort of names and alpha-conversion based upon multiple substitution, as well as of the system of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f4651b1e1370e231c4aba7048e266b93
https://doi.org/10.1016/j.entcs.2020.08.010
https://doi.org/10.1016/j.entcs.2020.08.010
Publikováno v:
LSFA
In this article we continue the work started in [Ernesto Copello, Alvaro Tasistro, Nora Szasz, Ana Bove, and Maribel Fernandez. Alpha-structural induction and recursion for the λ-calculus in constructive type theory. Electronic Notes in Theoretical
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::bde398a07656bda17928c81ddf9ceb8f
https://doi.org/10.1016/j.entcs.2018.10.006
https://doi.org/10.1016/j.entcs.2018.10.006
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 274, Iss Proc. LFMTP 2018, Pp 11-26 (2018)
LFMTP@FSCD
LFMTP@FSCD
We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then define a generic alpha-equivalence relation over the types of the uni
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6b60c0fce450ee82965d283572c1f166
https://doaj.org/article/fa5114a1eeab49e8a7ee3d22bb0b8bb3
https://doaj.org/article/fa5114a1eeab49e8a7ee3d22bb0b8bb3
Publikováno v:
Theoretical Computer Science. 685:65-82
We develop metatheory of the Lambda calculus in Constructive Type Theory, using a first-order presentation with one sort of names for both free and bound variables and without identifying terms up to α -conversion. Concerning β -reduction, we prove
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::bbda5347848e0d1fe760ca4651328e1c
https://doi.org/10.1016/j.tcs.2016.08.025
https://doi.org/10.1016/j.tcs.2016.08.025
Publikováno v:
Revista Latinoamericana de Ingeniería de Software, Vol 1, Iss 5, Pp 153-166 (2013)
El desarrollo de software se ha vuelto una actividad muy importante en el mundo actual. Existen numeros procesos de desarrollo de software que buscan aumentar la calidad de los productos y disminuir los tiempos de salida al mercado. Sin embargo, el s
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ae8ef2385dd689d02e9ce36810c05adf
http://www.unla.edu.ar/sistemas/redisla/ReLAIS/relais-v1-n5-p-153-166.pdf
http://www.unla.edu.ar/sistemas/redisla/ReLAIS/relais-v1-n5-p-153-166.pdf
Publikováno v:
Programming Languages ISBN: 9783319118628
SBLP
SBLP
We present a full certification of merge sort in the language Agda. It features: termination warrant without explicit proof, no proof cost to ensure that the output is sorted, and a succinct proof that the output is a permutation of the input.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::44ce4d830a818d42cb56ec12d3751ffa
https://doi.org/10.1007/978-3-319-11863-5_5
https://doi.org/10.1007/978-3-319-11863-5_5
Autor:
Jorge Pais, Álvaro Tasistro
Publikováno v:
Learning and Collaboration Technologies. Designing and Developing Novel Learning Experiences ISBN: 9783319074818
HCI (14)
HCI (14)
We present a proof assistant designed to help learning formal proof, particularly in the system of Natural Deduction for First-Order Logic. The assistant handles formulas and derivations containing meta-variables and allows to maintain a library of i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2e06f15140a8c129361e21942af4d74b
https://doi.org/10.1007/978-3-319-07482-5_42
https://doi.org/10.1007/978-3-319-07482-5_42