A Certified Functional Nominal C-Unification Algorithm

2020 ◽  
pp. 123-138 ◽  
Author(s):  
Mauricio Ayala-Rincón ◽  
Maribel Fernández ◽  
Gabriel Ferreira Silva ◽  
Daniele Nantes-Sobrinho
Keyword(s):  
Unification Algorithm

Analysis of Service Compatibility

2010 ◽  
pp. 136-155
Author(s):  
Ken Q. Pu
Keyword(s):  
Relational Database ◽  
Type System ◽  
Large Family ◽  
Service Description ◽  
Worst Case ◽  
Database Queries ◽  
Unification Algorithm ◽  
Data Services ◽  
Wide Range ◽  
Unification Problem

In this chapter, the authors apply type-theoretic techniques to the service description and composition verification. A flexible type system is introduced for modeling instances and mappings of semi-structured data, and is demonstrated to be effective in modeling a wide range of data services, ranging from relational database queries to web services for XML. Type-theoretic analysis and verification are then reduced to the problem of type unification. Some (in)tractability results of the unification problem and the expressiveness of their proposed type system are presented in this chapter. Finally, the auhtors construct a complete unification algorithm which runs in EXP-TIME in the worst case, but runs in polynomial time for a large family of unification problems rising from practical type analysis of service compositions.

scholarly journals A polynomial nominal unification algorithm

2008 ◽  
Vol 403 (2-3) ◽  
pp. 285-306 ◽  
Author(s):  
Christophe Calvès ◽  
Maribel Fernández
Keyword(s):  
Unification Algorithm

scholarly journals Type Reconstruction for Type Classes

1995 ◽  
Vol 5 (2) ◽  
pp. 201-224 ◽  
Author(s):  
Tobias Nipkow ◽  
Christian Prehofer
Keyword(s):  
Programming Language ◽  
Functional Programming ◽  
Type Inference ◽  
Constraint Solving ◽  
Simple Type ◽  
Inference Problem ◽  
Unification Algorithm ◽  
Type Classes ◽  
Type Reconstruction ◽  
Inference Systems

AbstractWe study the type inference problem for a system with type classes as in the functional programming language Haskell. Type classes are an extension of ML-style polymorphism with overloading. We generalize Milner's work on polymorphism by introducing a separate context constraining the type variables in a typing judgement. This leads to simple type inference systems and algorithms which closely resemble those for ML. In particular, we present a new unification algorithm which is an extension of syntactic unification with constraint solving. The existence of principal types follows from an analysis of this unification algorithm.

scholarly journals Formal Correctness of a Quadratic Unification Algorithm

2006 ◽  
Vol 37 (1-2) ◽  
pp. 67-92 ◽  
Author(s):  
José-Luis Ruiz-Reina ◽  
Francisco-Jesús Martín-Mateos ◽  
José-Antonio Alonso ◽  
María-José Hidalgo
Keyword(s):  
Unification Algorithm

Complexity of the unification algorithm for first-order expressions

CALCOLO ◽  
1975 ◽  
Vol 12 (4) ◽  
pp. 361-371 ◽  
Author(s):  
M. Venturini Zilli
Keyword(s):  
Unification Algorithm ◽  
First Order
Sign in / Sign up

Export Citation Format

Share Document