Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)

Autor: Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

Publikováno v: Logical Methods in Computer Science, Vol Volume 19, Issue 4 (2023)

We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail, a new non-deterministic calculus in which intersection types control r

Externí odkaz: https://doaj.org/article/0117e6998a2f401aa9443b06066087df

Elementary Deduction Problem for Locally Stable Theories with Normal Forms

Autor: Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho

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

Formalising nominal C-unification generalised with protected variables

Autor: Mauricio Ayala-Rincón, Washington de Carvalho-Segundo, Maribel Fernández, Daniele Nantes-Sobrinho, Gabriel Ferreira Silva

Publikováno v: Mathematical Structures in Computer Science. 31:286-311

This work extends a rule-based specification of nominal C-unification formalised in Coq to include ‘protected variables’ that cannot be instantiated during the unification process. By introducing protected variables, we are able to reuse the C-un

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::9941d542ca5fc4ea9ce5b65ffc80e162
https://doi.org/10.1017/s0960129521000050

Desunificação Nominal via Ponto Fixo

Autor: Daniele Nantes-Sobrinho, Leonardo Batista

Publikováno v: Anais do II Workshop Brasileiro de Lógica (WBL 2021).

Este é um trabalho em andamento sobre a resolução de equações e diferenças entre termos nominais, chamado de problema de desunificação nominal. Ao invés de usarmos as técnicas nominais padrões que envolvem restrições de freshness (i.e.,

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::f7cc591ef6d714ea0c9990e845afd059
https://doi.org/10.5753/wbl.2021.15773

A formalisation of nominal α-equivalence with A, C, and AC function symbols

Autor: Daniele Nantes-Sobrinho, Maribel Fernández, Washington de Carvalho-Segundo, Ana Cristina Rocha-Oliveira, Mauricio Ayala-Rincón

Publikováno v: Ayala-Rincón, M, de Carvalho-Segundo, W, Fernández, M, Nantes-Sobrinho, D & Rocha-Oliveira, A C 2019, ' A formalisation of nominal α-equivalence with A, C, and AC function symbols ', Theoretical Computer Science, vol. 781, pp. 3-23 . https://doi.org/10.1016/j.tcs.2019.02.020

This paper describes a formalisation in Coq of nominal syntax extended with associative (A), commutative (C) and associative-commutative (AC) operators. This formalisation is based on a natural notion of nominal α-equivalence, avoiding the use of an

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::22067b4d5ee67a37ee4d3c94b8c193bd
https://doi.org/10.1016/j.tcs.2019.02.020