Description

Welcome! This page contains PVS and Coq specifications and formalisations for the nominal setting, done by the computer science theory group of University of Brasília (UnB) - Brazil.

The nominal theory in PVS, also available at the PVS NASAlib.

• The theory nominalunif contains four main developments. The first one is a specification for a functional nominal unification algorithm. The second is a specification for a functional nominal C-unification and C-matching algorithm, through protected variables. The third refers to a work published in LOPSTR 2019, that contains only the nominal C-unification and its implementation in Python. The four refers to the first formalization of Stickes-Fages AC-unification algorith, and its application to nominal AC-matching.

Theory in Coq:

• A formalisation, in Coq, of nominal C-unification and nominal A, C and AC-equivalence. A set of inductive inference rules is used.

Download

• nominalunif is available for PVS 6.0


• CoqNominal has been compiled for Coq 8.7.2

Related work

• Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Temur Kutsia, Daniele Nantes-Sobrinho: Nominal AC-Matching (Best Paper Prize) Proc. 16th International Conference on Intelligent Computer Mathematics, (CICM), LNCS 14101:53-68 (2023)


• Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Daniele Nantes Sobrinho: A Certified Algorithm for AC-Unification Proc. 7th International Conference on Formal Structures for Computation and Deduction, (FSCD), LIPIcs 228:8:1--8:21 (2022)


• Mauricio Ayala-Rincón, Washington de Carvalho Segundo, Maribel Fernández, Gabriel Ferreira Silva, Daniele Nantes-Sobrinho: Formalising nominal C-unification generalised with protected variables Math. Struct. Comput. Sci. 31(3): 286-311 (2021)


• Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Daniele Nantes-Sobrinho: A Certified Functional Nominal C-Unification Algorithm Proc. 29th International Symposium on Logic-Based Program Synthesis and Transformation, {LOPSTR} 2019, Revised Selected Papers, LNCS 12042:123--138 (2020)


• Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho: On Nominal Syntax and Permutation Fixed Points CoRR abs/1902.08345, Logical Methods in Computer Science, 19(1):19:1-36 (2020)


• Mauricio Ayala-Rincón, Washington de Carvalho Segundo, Maribel Fernández, Daniele Nantes-Sobrinho: A Formalisation of Nominal C-Matching through Unification with Protected Variables Electr. Notes Theor. Comput. Sci. 344: 47-65 (2019)


• Mauricio Ayala-Rincón, Washington de Carvalho Segundo, Maribel Fernández, Daniele Nantes-Sobrinho, Ana Cristina Rocha Oliveira: A formalisation of nominal alpha-equivalence with A, C, and AC function symbols. Theor. Comput. Sci. 781: 3-23 (2019)


• Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho and Deivid Vale: On Solving Nominal Disunification Constraints. Proc Logical and Semantic Frameworks with Applications, LSFA 2019, Electr. Notes Theor. Comput. Sci. 348:3-22 (2019).


• Mauricio Ayala-Rincón, Maribel Fernández, Ana Cristina Rocha Oliveira, Daniel Lima Ventura: Nominal essential intersection types. Theor. Comput. Sci. 737: 62-80 (2018)


• Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho: Fixed-Point Constraints for Nominal Equational Unification. FSCD 2018, LIPIcs Vol. 108:7:1-16, 2018


• Mauricio Ayala-Rincón, Washington de Carvalho Segundo, Maribel Fernández, Daniele Nantes-Sobrinho: On Solving Nominal Fixpoint Equations. FroCoS 2017, LNCS Vol. 10483:209-226, 2017


• Mauricio Ayala-Rincón, Washington de Carvalho Segundo, Maribel Fernández, Daniele Nantes-Sobrinho: Nominal C-Unification. LOPSTR 2017, LNCS Vol. 10855:235-251, 2018


• Mauricio Ayala-Rincón, Maribel Fernández, Murdoch James Gabbay, Ana Cristina Rocha Oliveira: Checking Overlaps of Nominal Rewriting Rules. Electr. Notes Theor. Comput. Sci. 323: 39-56 (2016)


• Mauricio Ayala-Rincón, Maribel Fernández, Ana Cristina Rocha Oliveira: Completeness in PVS of a Nominal Unification Algorithm. Electr. Notes Theor. Comput. Sci. 323: 57-74 (2016)


• Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho: Nominal Narrowing. FSCD 2016: LIPIcs Vol. 52:11:1-17, 2016

Work in Progress

• To be included in brief!

Contact

The main authors are Mauricio Ayala-Rincón, Maribel Fernandez, Ana Cristina Rocha Oliveira , Washington de Carvalho Segundo, Gabriel Ferreira Silva, Daniele Nantes Sobrinho and Deivid Vale.