| dc.relation | [1] T. Aoto and K. Kikuchi. Nominal Confluence Tool. In Proc. of the 8th Int. Joint Conf.:
Automated Reasoning (IJCAR), volume 9706 of LNCS, pages 173–182. Springer, 2016.
4
[2] A. B. Avelar, A. L. Galdino, F. L. C. de Moura, and M. Ayala-Rincón. First-order
unification in the PVS proof assistant. Logic Journal of the IGPL, 22(5):758–789,
2014. 5
[3] M. Ayala-Rincón, W. Carvalho-Segundo, M. Fernández, and D. Nantes-Sobrinho.
Nominal C-Unification. In Proc. of the 27th Int. Symp. Logic-Based Program Synthesis
and Transformation (LOPSTR), volume 10855 of LNCS, pages 235–251. Springer,
2017. 5, 7, 72, 107
[4] M. Ayala-Rincón, W. Carvalho-Segundo, M. Fernández, and D. Nantes-Sobrinho. On
Solving Nominal Fixpoint Equations. In Proc. of the 11th Int. Symp. on Frontiers of
Combining Systems (FroCoS), volume 10483 of LNCS, pages 209–226. Springer, 2017.
7, 107
[5] M. Ayala-Rincón, W. de Carvalho Segundo, M. Fernández, and D. Nantes-Sobrinho.
A formalisation of nominal -equivalence with A and AC function symbols. ENTCS,
332:21–38, 2017. 6, 44
[6] M. Ayala-Rincón, W. de Carvalho Segundo, M. Fernández, and D. Nantes-Sobrinho.
A Formalisation of Nominal -equivalence with A, C, and AC Function Symbols.
TCS, 2019. Accepted manuscript in Theoretical Computer Science. 6, 44
[7] M. Ayala-Rincón, M. Fernández, W. Carvalho-Segundo, and D. Nantes-Sobrinho. A
Formalisation of Nominal C-Matching through Unification with Protected Variables.
In Pre-proc. of Logical and Semantic Frameworks with Applications (LSFA), to appear
in ENTCS, pages 29–41. Elseviser, 2018. 7, 72
[8] M. Ayala-Rincón, M. Fernández, M. J. Gabbay, and A. C. Rocha Oliveira. Checking
Overlaps of Nominal Rewriting Rules. ENTCS, 323:39–56, 2016. 4
[9] M. Ayala-Rincón, M. Fernández, and D. Nantes-Sobrinho. Nominal Narrowing. In
Proc. of the 1st Int. Conf. on Formal Structures for Computation and Deduction
(FSCD), volume 52 of LIPIcs, pages 11:1–11:17. SDLZI, 2016. 6
[10] M. Ayala-Rincón, M. Fernández, and D. Nantes-Sobrinho. Fixed-Point Constraints for
Nominal Equational Unification. In Proc. of the 3rd Int. Conf. on Formal Structuresfor Computation and Deduction (FSCD), volume 108 of LIPIcs, pages 7:1–7:16. SDLZI,
2018. 7, 148
[11] M. Ayala-Rincón, M. Fernández, and A. C. Rocha-oliveira. Completeness in PVS of
a Nominal Unification Algorithm. ENTCS, 323:57–74, 2016. 5, 32
[12] M. Ayala-Rincón, M. Fernández, A. C. Rocha-Oliveira, and D. L. Ventura. Nominal
essential intersection types. Theoretical Computuper Science, 737:62–80, 2018. 5
[13] B. Aydemir, A. Bohannon, and S. Weirich. Nominal Reasoning Techniques in Coq.
ENTCS, 174(5):69–77, 2007. 6
[14] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge UP, 1998. 19
[15] F. Baader and W. Snyder. Unification Theory. In Handbook of Automated Reasoning
(in 2 volumes), pages 445–532. Elsevier and MIT Press, 2001. 3
[16] A. Baumgartner, T. Kutsia, J. Levy, and M. Villaret. Nominal Anti-Unification. In
Rewriting Techniques and Applications, (RTA), pages 57–73. SDLZI, 2015. 4
[17] D. Benanav, D. Kapur, and P. Narendran. Complexity of Matching Problems. J. of
Sym. Computation, 3(1/2):203–216, 1987. 3, 22, 62, 71
[18] A. Boudet and E. Contejean. AC-Unification of Higher-Order Patterns. In Proc. of
Principles and Practice of Constraint Programming, volume 1330 of LNCS, pages
267–281. Springer, 1997. 148
[19] A. Boudet, E. Contejean, and H. Devie. A New AC Unification Algorithm with an
Algorithm for Solving Systems of Diophantine Equations. Logic in Computer Science,
pages 289–299, 1990. 3
[20] T. Braibant and D. Pous. Tactics for Reasoning Modulo AC in Coq. In In Proc. of
the 1st. Int. Conf. on Certified Programs and Proofs (CPP), volume 7086 of LNCS,
pages 167–182. Springer, 2011. 6
[21] K. F. Brandt, A. Schlichtkrull, and J. Villadsen. Formalization of First-Order Syntactic
Unification. In Pre-proc. of the 32nd Int. Workshop on Unification (UNIF), 2018. 5
[22] W. E. Byrd and D. P. Friedman. Kanren: A Fresh Name in Nominal Logic
Programming. In Proc. of the Workshop on Scheme and Functional Programming,
pages 79–90, 2007. 4
[23] C. F. Calvès. Complexity and implementation of nominal algorithms. PhD Thesis,
King’s College London, 2010. 4
[24] C. F. Calvès and M. Fernández. Matching and Alpha-Equivalence Check for Nominal
Terms. J. of Computer and System Sciences, 76(5):283–301, 2010. 4, 64, 69, 70
[25] C. F. Calvès and M. Fernández. The First-order Nominal Link. In Proc. of the 20th
Int. Symp. Logic-based Program Synthesis and Transformation (LOPSTR), volume
6564 of LNCS, pages 234–248. Springer, 2011. 4, 31[26] J. Cheney. Prolog User’s Guide & Language Reference Version 0.3 DRAFT, 2003. 4
[27] J. Cheney. Relating nominal and higher-order pattern unification. Proceedings of the
19th international workshop on Unification (UNIF 2005), 2005. 4
[28] J. Cheney. Equivariant unification. J. of Autom. Reasoning, 45(3):267–300, 2010. 4
[29] M. Clausen and A. Fortenbacher. Efficient Solution of Linear Diophantine Equations.
J. of Sym. Computation, 8(1-2):201–216, 1989. 3
[30] E. Contejean. A Certified AC Matching Algorithm. In Proc. of the 15th Int. Conf.
on Rewriting Techniques and Applications (RTA), volume 3091 of LNCS, pages 70–84.
Springer, 2004. 6, 133
[31] E. Copello, E. Tasistro, N. Szasz, A. Bove, and M. Fernández. Principles of Alpha-
Induction and Recursion for the Lambda Calculus in Constructive Type Theory.
ENTCS, 323:109–124, 2016. 6
[32] CoqTeam. The Coq Proof Assistant Reference Manual, 2019. 32
[33] T. H. Cormen, C. E. Leiserson, R. Rivest, and C. Stein. Introduction to Algorithms.
The MIT Press, 2009. 71
[34] R. Di Cosmo. Second Order Isomorphic Types: A Proof Theoretic Study on Second
Order lambda-Calculus with Surjective Paring and Terminal Object. Inf. Comput.,
119(2):176–201, 1995. 149
[35] F. Durán, S. Eker, S. Escobar, N. Martí-Oliet, J. Meseguer, and C. L. Talcott.
Associative unification and symbolic reasoning modulo associativity in maude. In
Proc. of Rewriting Logic and Its Applications (WLRA), volume 11152 of LNCS, pages
98–114. Springer, 2018. 6
[36] S. M. Eker. Associative-Commutative Matching Via Bipartite Graph Matching. The
Computer J., 38:381–399, 1995. 3
[37] S. M. Eker. Associtative-Commutative Rewriting on Large Terms. In Rewriting
Techniques and Applications, (RTA), volume 2706 of LNCS, pages 14–29, 2003. 3
[38] François Fages. Associative-Commutative Unification. J. of Sym. Computation,
3:257–275, 1987. 3, 22
[39] E. Fairweather, M. Fernández, N. Szasz, and A. Tasistro. Dependent Types for
Nominal Terms with Atom Substitutions. In Int. Conf. on Typed Lambda Calculi and
Applications, (TLCA), pages 180–195. SDLZI, 2015. 5
[40] M. Fernández and M. Gabbay. Curry-Style Types for Nominal Terms. In Int. Work.
on Types for Proofs and Programs (TYPES), volume 4502 of LNCS, pages 125–139.
Springer, 2006. 5
[41] M. Fernández and M. J. Gabbay. Nominal Rewriting. Information and Computation,
205(6):917–965, 2007. 4, 5[42] M. J. Gabbay and A. M. Pitts. A New Approach to Abstract Syntax with Variable
Binding. Formal Aspects of Computing, 13(3-5):341–363, 2002. 3
[43] D. Kapur and P. Narendran. NP-Completeness of the Set Unification and Matching
Problems. In 8th International Conference on Automated Deduction (CADE), volume
230 of LNCS, pages 489–495. Springer, 1986. 3, 22
[44] D. Kapur and P. Narendran. Matching, Unification and Complexity. SIGSAM
Bulletin, 21(4):6–9, 1987. 3, 22
[45] D. Kapur and P. Narendran. Complexity of Unification Problems with Associative-
Commutative Operators. J. of Autom. Reasoning, 9(2):261–288, 1992. 3, 22
[46] R. Kumar and M. Norrish. (Nominal) Unification by Recursive Descent with Triangular
Substitutions. In Proc. of the 1st Int. Conf. of Interactive Theorem Proving (ITP),
volume 6172 of LNCS, pages 51–66. Springer, 2010. 5
[47] D. Larchey-Wendling and J.-F. Monin. Simulating Induction-Recursion for Partial Algorithms.
Accepted to TYPES. Available at https://members.loria.fr/DLarchey/
files/papers/TYPES_2018_paper_19.pdf, 2018. 61
[48] J. Levy and M. Villaret. An Efficient Nominal Unification Algorithm. In Proc. of the
21st Int. Conf. on Rewriting Techniques and Applications (RTA), volume 6 of LIPIcs,
pages 209–226. SDLZI, 2010. 4, 31
[49] J. Levy and M. Villaret. Nominal unification from a higher-order perspective. ACM
Trans. Comput. Log., 13(2):10:1–10:31, 2012. 4
[50] G. S. Makanin. The Problem of Solvability of Equations in a Free Semigroup. Math.
USSR Sbornik, 32(2):129–198, 1977. 17, 22, 149
[51] A Martelli and U. Montanari. Unification in linear time and space: A structured
presentation. Technical report, Ist. di Elaborazione delle Informazione, Consiglio
Nazionale delle Ricerche, Pisa, Italy, 1976. Internal Rep. B76-16. 3, 16, 22
[52] A. Martelli and U. Montanari. An Efficient Unification Algorithm. ACM Transactions
on Programming Languages and Systems, 4(2):258–282, 1982. 16
[53] D. Miller. A logic programming language with lambda-abstraction, function variables,
and simple unification. J. Log. Comput., 1(4):497–536, 1991. 4
[54] T. Nipkow. Equational Reasoning in Isabelle. Science of Computer Programming,
12(2):123–149, 1989. 6
[55] T. Nipkow. Functional unification of higher-order patterns. In Proc. of the Eighth
Annual Symp. on Logic in Computer Science (LICS), pages 64–74. IEEE, 1993. 4
[56] M. S. Paterson and M. N. Wegman. Linear Unification. J. of Computer and System
Sciences, 16(2):158–167, 1978. 3, 4, 16, 22
[57] A. M. Pitts. Nominal Logic, a First Order Theory of Names and Binding. Information
and Computation, 186(2):165–193, 2003. 3, 22[58] A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge
UP, 2013. 3
[59] Z. Qian and K. Wang. Modular AC unification of higher-order patterns. In Proc. of
the First Int. Conf. Constraints in Computational Logics, volume 845 of LNCS, pages
105–120. Springer, 1994. 148
[60] J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. J. of
the ACM, 12(1):23–41, 1965. 3, 13, 22
[61] A. C. Rocha-Oliveira. Unificação, confluência e tipos com interseção para sistemas de
reescrita nominal. PhD thesis, Universidade de Brasília (UnB), 2016. 5, 32
[62] Sagan, B. E. The Symmetric Group: Representations, Combinatorial Algorithms, and
Symmetric Functions. Springer, 2nd edition, 2001. 107
[63] M. Schmidt-Schauß, T. Kutsia, J. Levy, and M. Villaret. Nominal Unification of
Higher Order Expressions with Recursive Let. In Post-proc. of the 26th Int. Sym. on
Logic-Based Program Synthesis and Transformation (LOPSTR 2016), volume 10184
of LNCS, pages 328–344. Springer, 2017. 7
[64] J. H. Siekmann. Unification of Commutative Terms. In Proc. of the Int. Symposium
on Symbolic and Algebraic Manipulation, volume 72 of LNCS, pages 22–29. Springer,
1979. 3, 18
[65] M. Sozeau. Subset Coercions in Coq. In Proc. of the Int. Work. on Types for Proofs
and Programs (TYPES), volume 4502 of LNCS, pages 237–252. Springer, 2006. 61
[66] M. Sozeau. Equations: A Dependent Pattern-Matching Compiler. In Proc. of the
1st Int. Conf. of Interactive Theorem Proving (ITP), volume 6172 of LNCS, pages
419–434. Springer, 2010. 58
[67] M. E. Stickel. A Unification Algorithm for Associative-Commutative Functions. J. of
the Association for Computing Machinery, 28(3):423–434, 1981. 3, 19, 22
[68] E. Tiden and S. Arnborg. Unification Problems with One-Sided Distributivity. J. of
Sym. Computation, 3:183–202, 1987. 22
[69] C. Urban. Nominal Techniques in Isabelle/HOL. J. of Autom. Reasoning, 40(4):327–
356, 2008. 5
[70] C. Urban. Nominal Unification Revisited. In Proc. of the 24th Int. Work. on
Unification (UNIF), volume 42 of EPTCS, pages 1–11, 2010. 5, 32
[71] C. Urban and C. Kaliszyk. General Bindings an Alpha-Equivalence in Nominal
Isabelle. Logical Methods in Computer Science, 8:1–35, 2012. 6
[72] C. Urban, A. M. Pitts, and M. J. Gabbay. Nominal Unification. Theoretical Computer
Science, 323(1-3):473–497, 2004. 3, 4, 5, 26, 31, 32
[73] Z. Qian. Linear Unification of Higher-Order Patterns. Theory and Practice of Software
Development, pages 391–405, 1993. 4 | |
