Zobrazeno 1 - 10
of 144
pro vyhledávání: '"Mauricio Ayala-Rincón"'
Publikováno v:
Logical Methods in Computer Science, Vol Volume 16, Issue 1 (2020)
We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive no
Externí odkaz:
https://doaj.org/article/314aee7c8c70479aa6f0762523e3042b
Autor:
Mauricio Ayala-Rincón
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 204, Iss Proc. DCM 2015, Pp 11-17 (2016)
Confluence is a critical property of computational systems which is related with determinism and non ambiguity and thus with other relevant computational attributes of functional specifications and rewriting system as termination and completion. Seve
Externí odkaz:
https://doaj.org/article/a9ee09074b604cf1bca81199d90084ea
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 113, Iss Proc. LSFA 2012, Pp 45-60 (2013)
We present an algorithm to decide the intruder deduction problem (IDP) for a class of locally stable theories enriched with normal forms. Our result relies on a new and efficient algorithm to solve a restricted case of higher-order associative-commut
Externí odkaz:
https://doaj.org/article/2684a69b0a2841f49c034b12280b0410
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 113, Iss Proc. LSFA 2012, Pp 145-152 (2013)
Orthogonality is a discipline of programming that in a syntactic manner guarantees determinism of functional specifications. Essentially, orthogonality avoids, on the one side, the inherent ambiguity of non determinism, prohibiting the existence of d
Externí odkaz:
https://doaj.org/article/8dc8a612c3d1410ba570417bf46914d2
Publikováno v:
Journal of Formalized Reasoning, Vol 6, Iss 1, Pp 31-61 (2013)
In this work, we present an algebraic approach for modeling the two-party cascade protocol of Dolev-Yao and for fully formalizing its security in the specification language of the Prototype Verification System PVS. Although cascade protocols could be
Externí odkaz:
https://doaj.org/article/767e571c84044efa805d9f4f91c1d389
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 81, Iss Proc. LSFA 2011, Pp 63-78 (2012)
This work presents a formalization of the theorem of existence of most general unifiers in first-order signatures in the higher-order proof assistant PVS. The distinguishing feature of this formalization is that it remains close to the textbook proof
Externí odkaz:
https://doaj.org/article/d2ce367afa5846a39a22e7c4e7c54628
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 15, Iss Proc. WRS 2009, Pp 69-82 (2010)
The lambda-calculus with de Bruijn indices assembles each alpha-class of lambda-terms in a unique term, using indices instead of variable names. Intersection types provide finitary type polymorphism and can characterise normalisable lambda-terms thro
Externí odkaz:
https://doaj.org/article/f5152fa8be584456b6bfc16fc32663b3
Publikováno v:
Journal of Formalized Reasoning, Vol 1, Iss 1, Pp 39-50 (2008)
This paper shows how a formalization for the theory of Abstract Reduction Systems (ARSs) in which noetherianity was specified by the notion of well-foundness over binary relations is used in order to prove results such as the well-known Newman's and
Externí odkaz:
https://doaj.org/article/05bd7249a9bc425783a856c7255f5dbf
Publikováno v:
Journal of Automated Reasoning. 66:1031-1063
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8a307b6a048ccc8c132dd22e982f9d2f
https://doi.org/10.1007/s10817-021-09615-x
https://doi.org/10.1007/s10817-021-09615-x
Publikováno v:
Journal of Automated Reasoning. 65:1231-1263
This paper presents a PVS development of relevant results of the theory of rings. The PVS theory includes complete proofs of the three classical isomorphism theorems for rings, and characterizations of principal, prime and maximal ideals. Algebraic c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::aefafd3f76ad0539d92a776066ac7b88
https://doi.org/10.1007/s10817-021-09593-0
https://doi.org/10.1007/s10817-021-09593-0