Stem unif$ (all stems)

261 papers:

ICFP-2015-ZilianiS #algorithm #coq #morphism #polymorphism #unification

A unification algorithm for Coq featuring universe polymorphism and overloading (BZ, MS), pp. 179–191.

CADE-2015-BackemanR #bound #proving #theorem proving

Theorem Proving with Bounded Rigid E-Unification (PB, PR), pp. 572–587.

CADE-2015-Libal #higher-order #unification

Regular Patterns in Second-Order Unification (TL), pp. 557–571.

CAV-2015-AlurCR #synthesis #unification

Synthesis Through Unification (RA, PC, AR), pp. 163–179.

CSL-2015-GasconST #polynomial #strict #unification

Two-Restricted One Context Unification is in Polynomial Time (AG, MSS, AT), pp. 405–422.

LICS-2015-GasconTS #polynomial #problem #unification

One Context Unification Problems Solvable in Polynomial Time (AG, AT, MSS), pp. 499–510.

RTA-2015-BaumgartnerKLV #anti

Nominal Anti-Unification (AB, TK, JL, MV), pp. 57–73.

RTA-2015-KotsireasKS #design #equation #orthogonal #unification

Constructing Orthogonal Designs in Powers of Two: Gröbner Bases Meet Equational Unification (ISK, TK, DES), pp. 241–256.

FoSSaCS-2014-ErbaturKMMNR #on the #problem #symmetry #unification

On Asymmetric Unification and the Combination Problem in Disjoint Theories (SE, DK, AMM, CM, PN, CR), pp. 274–288.

CSMR-WCRE-2014-KrishnanT #refactoring #unification

Unification and refactoring of clones (GPK, NT), pp. 104–113.

ICALP-v2-2014-Jez #unification

Context Unification is in PSPACE (AJ), pp. 244–255.

PPDP-2014-YangEMMN #encryption #finite #unification

Theories of Homomorphic Encryption, Unification, and the Finite Variant Property (FY, SE, CM, JM, PN), pp. 123–133.

RTA-TLCA-2014-AubertB #unification

Unification and Logarithmic Space (CA, MB), pp. 77–92.

LATA-2013-AotoI #calculus #rule-based #termination

Termination of Rule-Based Calculi for Uniform Semi-Unification (TA, MI), pp. 56–67.

KDIR-KMIS-2013-SaidiDZC #process #requirements #semantics #towards #unification #using

Towards Unification of Requirements Engineering Approaches using Semantics-based Process (IES, TD, NZ, PJC), pp. 443–450.

CADE-2013-ErbaturEKLLMMNSS #analysis #encryption #paradigm #protocol #symmetry #unification

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis (SE, SE, DK, ZL, CL, CM, JM, PN, SS, RS), pp. 231–248.

RTA-2013-BaumgartnerKLV #anti #higher-order

A Variant of Higher-Order Anti-Unification (AB, TK, JL, MV), pp. 113–127.

RTA-2013-Calves #unification

Unifying Nominal Unification (CC), pp. 143–157.

RTA-2013-SmolkaT #recursion #unification

Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification (GS, TT), pp. 271–286.

LATA-2012-AnantharamanBNR #unification

Unification Modulo Chaining (SA, CB, PN, MR), pp. 70–82.

KR-2012-BaaderBM #towards #unification

Extending Unification in EL Towards General TBoxes (FB, SB, BM).

ECMFA-2012-VarroAS #pattern matching #unification

Unification of Compiled and Interpreter-Based Pattern Matching Techniques (GV, AA, AS), pp. 368–383.

ICLP-2012-BryS #query #semistructured data #simulation #unification

Simulation Unification: Beyond Querying Semistructured Data (Invited Talk) (FB, SS), pp. 1–13.

IJCAR-2012-AnantharamanELNR #unification

Unification Modulo Synchronous Distributivity (SA, SE, CL, PN, MR), pp. 14–29.

IJCAR-2012-BaaderBM #encoding #ontology #satisfiability #strict #unification

SAT Encoding of Unification in ℰℒℋ_R⁺ w.r.t. Cycle-Restricted Ontologies (FB, SB, BM), pp. 30–44.

IJCAR-2012-BaaderMM #logic #named #unification

UEL: Unification Solver for the Description Logic ℰℒ — System Description (FB, JM, BM), pp. 45–51.

IJCAR-2012-MarshallN #algorithm #unification

New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants (AMM, PN), pp. 408–422.

RTA-2012-CreusGG #unification

One-context Unification with STG-Compressed Terms is in NP (CC, AG, GG), pp. 149–164.

ITiCSE-2011-GarciaMGH #interface #learning #unification

A system for usable unification of interfaces of learning objects in m-learning (EG, LdM, AGC, JRH), p. 347.

ICEIS-v1-2011-MessaoudFKZ #documentation #unification #xml

Unification of XML Document Structures for Document Warehouse (DocW) (IBM, JF, KK, GZ), pp. 85–94.

PPDP-2011-EscobarKLMMNS #analysis #encryption #protocol #unification #using

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption (SE, DK, CL, CM, JM, PN, RS), pp. 65–76.

SAC-2011-Jamil #graph #query #unification #using

Computing subgraph isomorphic queries using structural unification and minimum graph structures (HMJ), pp. 1053–1058.

CADE-2011-BaaderBBM #concept #logic #unification

Unification in the Description Logic EL without the Top Concept (FB, TBN, SB, BM), pp. 70–84.

CADE-2011-LiuL #morphism #performance #unification

Efficient General Unification for XOR with Homomorphism (ZL, CL), pp. 407–421.

RTA-2011-DuranEEMT #maude #reachability #unification

Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6 (FD, SE, SE, JM, CLT), pp. 31–40.

RTA-2011-GasconMR #first-order #unification

First-Order Unification on Compressed Terms (AG, SM, LR), pp. 51–60.

RTA-2011-KutsiaLV

Anti-Unification for Unranked Terms and Hedges (TK, JL, MV), pp. 219–234.

TLCA-2011-AbelP #dependent type #higher-order #unification

Higher-Order Dynamic Pattern Unification for Dependent Types and Records (AA, BP), pp. 10–26.

RTA-2010-KutsiaM #order #regular expression #unification

Order-Sorted Unification with Regular Expression Sorts (TK, MM), pp. 193–208.

RTA-2010-LevyV #algorithm #performance #unification

An Efficient Nominal Unification Algorithm (JL, MV), pp. 209–226.

WRLA-2008-EscobarMS09 #equation #unification

Variant Narrowing and Equational Unification (SE, JM, RS), pp. 103–119.

FM-2009-Boute #logic #unification

Making Temporal Logic Calculational: A Tool for Unification and Discovery (RTB), pp. 387–402.

RTA-2009-BaaderM #logic #unification

Unification in the Description Logic EL (FB, BM), pp. 350–364.

RTA-2009-ClavelDEELMMT #maude #unification

Unification and Narrowing in Maude 2.4 (MC, FD, SE, SE, PL, NMO, JM, CLT), pp. 380–390.

RTA-2009-GasconGS #unification

Unification with Singleton Tree Grammars (AG, GG, MSS), pp. 365–379.

ICALP-A-2008-AzarG #framework #integer #source code #unification

Truthful Unification Framework for Packing Integer Programs with Choices (YA, IG), pp. 833–844.

PADL-2008-CoxN #array #logic programming #spreadsheet #unification

Unification of Arrays in Spreadsheets with Logic Programming (PTC, PKN), pp. 100–115.

IJCAR-2008-TourEN #equation #unification

Unification and Matching Modulo Leaf-Permutative Equational Presentations (TBdlT, ME, PN), pp. 332–347.

RTA-2008-LevyV #higher-order #perspective #unification

Nominal Unification from a Higher-Order Perspective (JL, MV), pp. 246–260.

LOPSTR-2007-ZhangN #constraints #scalability #theorem proving #unification #using

A Scalable Inclusion Constraint Solver Using Unification (YZ, FN), pp. 121–137.

SAC-2007-DjelloulDF #constraints #finite #first-order #infinity #prolog #theorem proving #towards #unification #using

Toward a first-order extension of Prolog’s unification using CHR: a CHR first-order constraint solver over finite or infinite trees (KD, TBHD, TWF), pp. 58–64.

RTA-2007-KutsiaLV #sequence #unification

Sequence Unification Through Currying (TK, JL, MV), pp. 288–302.

ICFP-2006-JonesVWW #data type #type inference

Simple unification-based type inference for GADTs (SLPJ, DV, SW, GW), pp. 50–61.

IJCAR-2006-LevySV #unification

Stratified Context Unification Is NP-Complete (JL, MSS, MV), pp. 82–96.

IJCAR-2006-Pientka #approach #higher-order #lightweight #unification

Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach (BP), pp. 362–376.

RTA-2006-LevySV #bound #higher-order #unification

Bounded Second-Order Unification Is NP-Complete (JL, MSS, MV), pp. 400–414.

SEKE-2005-BasitRJ #empirical #unification #using

An Empirical Study on Limits of Clone Unification Using Generics (HAB, DCR, SJ), pp. 109–114.

ECMDA-FA-2005-ChiversP #bidirectional #named

XRound: Bidirectional Transformations and Unifications Via a Reversible Template Language (HC, RFP), pp. 205–219.

PPDP-2005-LiL #unification

Inverting abstract unification for set-sharing (XL, LL), pp. 129–138.

CADE-2005-LevyNV #unification

Well-Nested Context Unification (JL, JN, MV), pp. 149–163.

ICLP-2005-NadathurL #higher-order #on the fly #unification

Practical Higher-Order Pattern Unification with On-the-Fly Raising (GN, NL), pp. 371–386.

RTA-2005-Cheney #unification

Equivariant Unification (JC), pp. 74–89.

RTA-2005-TourE #unification

Unification in a Class of Permutative Theories (TBdlT, ME), pp. 105–119.

ICALP-2004-Cheney #complexity #unification

The Complexity of Equivariant Unification (JC), pp. 332–344.

ICPR-v2-2004-YinFD #framework #unification

A Unification Framework for Tree and Block Wavelet Encoders (XWY, MF, ACD), pp. 795–798.

GPCE-2004-Schultz #automation #inheritance #unification

A Unification of Inheritance and Automatic Program Specialization (UPS), pp. 244–265.

RTA-2004-LevySV #higher-order #monad #unification

Monadic Second-Order Unification Is NP-Complete (JL, MSS, MV), pp. 55–69.

RTA-2004-MitsuhashiOOY #confluence #problem #unification

The Joinability and Unification Problems for Confluent Semi-constructor TRSs (IM, MO, YO, TY), pp. 285–300.

EDOC-2003-BurtBROA #data access #modelling #security #unification

Model Driven Security: Unification of Authorization Models for Fine-Grain Access Control (CCB, BRB, RRR, AMO, MA), pp. 159–173.

SIGIR-2003-Davison #analysis #towards #unification

Toward a unification of text and link analysis (BDD0), pp. 367–368.

CADE-2003-AnantharamanNR #morphism #unification

Unification Modulo ACU I Plus Homomorphisms/Distributivity (SA, PN, MR), pp. 442–457.

CADE-2003-ChoppellaH #unification

Source-Tracking Unification (VC, CTH), pp. 458–472.

CADE-2003-Lynch #problem #unification

Schematic Saturation for Decision and Unification Problems (CL), pp. 427–441.

CADE-2003-PientkaP #higher-order #optimisation #unification

Optimizing Higher-Order Pattern Unification (BP, FP), pp. 473–487.

RTA-2003-KapurNW #algorithm #composition #protocol

An E-unification Algorithm for Analyzing Protocols That Use Modular Exponentiation (DK, PN, LW), pp. 165–179.

ICPR-v3-2002-TanCM #image #named #retrieval #towards #unification

SmartAlbum — Towards Unification of Approaches for Image Retrieval (TT, JC, PM), pp. 983–986.

CSL-2002-Schmidt-SchaussS #bound #decidability #higher-order #unification

Decidability of Bounded Higher-Order Unification (MSS, KUS), pp. 522–536.

ICLP-2002-BryS #declarative #model transformation #query #semistructured data #simulation #towards #unification #xml

Towards a Declarative Query and Transformation Language for XML and Semistructured Data: Simulation Unification (FB, SS), pp. 255–270.

RTA-2002-LevyV #higher-order #problem #unification

Currying Second-Order Unification Problems (JL, MV), pp. 326–339.

ICFP-2001-Sheard #unification

Generic Unification via Two-Level Types and Parameterized Modules (TS), pp. 86–97.

SAC-2001-Jamil #relational #unification

A case for parameterized views and relational unification (HMJ), pp. 275–279.

CC-2001-KandemirU #array #locality #optimisation #unification

Array Unification: A Locality Optimization Technique (MTK), pp. 259–273.

CSL-2001-Schmidt-Schauss #unification

Stratified Context Unification Is in PSPACE (MSS), pp. 498–512.

RTA-2001-BoudetC #algorithm

Combining Pattern E-Unification Algorithms (AB, EC), pp. 63–76.

RTA-2001-LevyV #equation #traversal #unification

Context Unification and Traversal Equations (JL, MV), pp. 169–184.

RTA-2001-LynchM

Goal-Directed E-Unification (CL, BM), pp. 231–245.

RTA-2001-OyamaguchiO #confluence #problem #term rewriting #unification

The Unification Problem for Confluent Right-Ground Term Rewriting Systems (MO, YO), pp. 246–260.

PLDI-2000-Das #analysis #pointer

Unification-based pointer analysis with directional assignments (MD), pp. 35–46.

PPDP-2000-Ayala-RinconK #unification

Unification via se-style of explicit substitution (MAR, FK), pp. 163–174.

CADE-2000-Sofronie-Stokkermans #on the #unification

On Unification for Bonded Distributive Lattices (VSS), pp. 465–481.

CADE-2000-TiwariBR #revisited

Rigid E-Unification Revisited (AT, LB, HR), pp. 220–234.

RTA-2000-BjornerM #unification

Absolute Explicit Unification (NB, CM), pp. 31–46.

RTA-2000-LevyV #constraints #higher-order #linear #unification

Linear Second-Order Unification and Context Unification with Tree-Regular Constraints (JL, MV), pp. 156–171.

FoSSaCS-1999-DantsinV #algorithm #nondeterminism #polynomial #set #unification

A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees (ED, AV), pp. 180–196.

ICML-1999-UtgoffS #approximate #unification

Approximation Via Value Unification (PEU, DJS), pp. 425–432.

RTA-1999-KepserR #algorithm #equation #named #unification

UNIMOK: A System for Combining Equational Unification Algorithm (SK, JR), pp. 248–251.

IFL-1998-McAdam #interface #on the #unification

On the Unification of Substitutions in Type Interfaces (BJM), pp. 137–152.

ALP-PLILP-1998-LimetS #framework #problem

A General Framework for R-Unification Problems (SL, FS), pp. 266–281.

POPL-1998-Schubert #higher-order #morphism #polymorphism #type inference #unification

Second-Order Unification and Type Inference for Church-Style Polymorphism (AS), pp. 279–288.

CADE-1998-Beeson #unification #λ-calculus

Unification in Lambda-Calculi with if-then-else (MB), pp. 103–118.

CADE-1998-OliartS #algorithm #performance

A Fast Algorithm for Uniform Semi-Unification (AO, WS), pp. 239–253.

LICS-1998-Veanes #higher-order #unification

The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification (MV), pp. 264–275.

RTA-1998-DegtyarevGNVV #decidability

The Decidability of Simultaneous Rigid E-Unification with One Variable (AD, YG, PN, MV, AV), pp. 181–195.

RTA-1998-GuoNS #algebra #process #unification

Unification and Matching in Process Algebras (QG, PN, SKS), pp. 91–105.

RTA-1998-JacquemardMW #equation #unification

Unification in Extension of Shallow Equational Theories (FJ, CM, CW), pp. 76–90.

RTA-1998-Levy #decidability #higher-order #problem #unification

Decidable and Undecidable Second-Order Unification Problems (JL), pp. 47–60.

RTA-1998-Schmidt

E-Unification for Subsystems of S4 (RAS), pp. 106–120.

DAC-1997-SarrafzadehKT #unification

Unification of Budgeting and Placement (MS, DAK, GET), pp. 758–761.

ICALP-1997-GurevichV #monad #problem

Monadic Simultaneous Rigid E-Unification and Related Problems (YG, AV), pp. 154–165.

TOOLS-USA-1997-AllenHF #uml #unification

Method Unification: UML and OML (RA, BHS, DF), p. 372.

ALP-1997-KirchnerR #equation #higher-order #unification

Higher-Order Equational Unification via Explicit Substitutions (CK, CR), pp. 61–75.

LOPSTR-1997-ChasseurD #constraints #logic programming

Logic Program Schemas, Constraints, and Semi-unification (EC, YD), pp. 69–89.

CADE-1997-NiehrenPR #constraints #finite #on the #similarity #unification

On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting (JN, MP, PR), pp. 34–48.

ICLP-1997-AjiliK #composition #constraints #framework #unification

A Modular Framework for the Combination of Unification and Built-In Constraints (FA, CK), pp. 331–345.

LICS-1997-CervesatoP #higher-order #linear

Linear Higher-Order Pre-Unification (IC, FP), pp. 422–433.

LICS-1997-Goubault-Larrecq #higher-order #unification

Ramified Higher-Order Unification (JGL), pp. 410–421.

RTA-1997-Ringeissen #algorithm #programming language #prototype #rule-based #unification

Prototyping Combination of Unification Algorithms with the ELAN Rule-Based Programming Language (CR), pp. 323–326.

RTA-1997-Schulz #algorithm

A Criterion for Intractability of E-unification with Free Function Symbols and Its Relevance for Combination Algorithms (KUS), pp. 284–298.

CAiSE-1996-CastanoA #analysis #process #unification

Techniques for Process Analysis and Unification (SC, VDA), pp. 234–254.

CIKM-1996-Greco #bound #set #unification

Optimal Unification of Bounded Simple Set Terms (SG), pp. 326–336.

ALP-1996-FassbenderM #decidability #recursion #strict

A Strict Border for the Decidability of E-Unification for Recursive Functions (HF, SM), pp. 194–208.

CADE-1996-GuoNW #unification

Unification and Matching Modulo Nilpotence (QG, PN, DAW), pp. 261–274.

CADE-1996-HermannK #algorithm #polynomial #unification

Unification Algorithms Cannot be Combined in Polynomial Time (MH, PGK), pp. 246–260.

CADE-1996-Voronkov #logic #similarity

Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification (AV), pp. 32–46.

CADE-1996-Weidenbach #decidability #pseudo #unification

Unification in Pseudo-Linear Sort Theories is Decidable (CW), pp. 343–357.

JICSLP-1996-DowekHKP #higher-order #unification

Unification via Explicit Substitutions: The Case of Higher-Order Patterns (GD, TH, CK, FP), pp. 259–273.

LICS-1996-DegtyarevMV #algorithm #problem

Simultaneous E-Unification and Related Algorithmic Problems (AD, YM, AV), pp. 494–502.

RTA-1996-BoudetCM #proving #theorem proving #unification

AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.

RTA-1996-FettigL #finite #higher-order #unification #λ-calculus

Unification of Higher-Order patterns in a Simply Typed λ-Calculus with Finite Products and terminal Type (RF, BL), pp. 347–361.

RTA-1996-Levy #higher-order #linear #unification

Linear Second-Order Unification (JL), pp. 332–346.

RTA-1996-Schmidt-Schauss #algorithm #unification

An Algorithm for Distributive Unification (MSS), pp. 287–301.

SAS-1995-RaoS #execution #prolog #source code

Unification-Free Execution of Well-Moded and Well-Typed Prolog Programs (MRKKR, RKS), pp. 243–260.

LOPSTR-1995-ArtsZ #logic programming #semantics #source code #termination #unification #using

Termination of Logic Programs Using Semantic Unification (TA, HZ), pp. 219–233.

PLILP-1995-Arenas-SanchezD #set #unification

Minimal Set Unification (PAS, AD), pp. 397–414.

POPL-1995-DawsonRRSSSW #execution #logic programming #performance #source code #unification

Unification Factoring for Efficient Execution of Logic Programs (SD, CRR, IVR, KFS, SS, TS, DSW), pp. 247–258.

SAC-1995-AllenB #adaptation #parsing

A unification-based adaptive parser (CSA, BRB), pp. 282–287.

ILPS-1995-DawsonRRS #optimisation #unification

Optimizing Clause Resolution: Beyond Unification Factoring (SD, CRR, IVR, TS), pp. 194–208.

LICS-1995-DowekHK #higher-order #unification

Higher-Order Unification via Explicit Substitutions (Extended Abstract) (GD, TH, CK), pp. 366–374.

RTA-1995-Burghardt #set

Regular Substitution Sets: A Means of Controlling E-Unification (JB), pp. 382–396.

RTA-1995-OttoND #equation #independence #unification

Some Independent Results for Equational Unification (FO, PN, DJD), pp. 367–381.

ESOP-1994-Hanus #lazy evaluation #unification

Lazy Unification with Simplification (MH), pp. 272–286.

TAGT-1994-PlumpH #graph #unification

Graph Unification and Matching (DP, AH), pp. 75–88.

SIGIR-1994-JacqueminR #framework

Retrieving Terms and their Variants in a Lexicalised Unification-Based Framework (CJ, JR), pp. 132–141.

SAC-1994-LiB #object-oriented #parsing #unification

An integrated parsing scheme for unification categorial grammar with object-oriented lexicon (LL, BRB), pp. 524–528.

CADE-1994-Beckert

A Completion-Based Method for Mixed Universal and Rigid E-Unification (BB), pp. 678–692.

CADE-1994-JohannK #constant #order #unification #λ-calculus

Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading (PJ, MK), pp. 620–634.

CADE-1994-MullerW #composition #higher-order #theory and practice

Theory and Practice of Minimal Modular Higher-Order E-Unification (OM, FW), pp. 650–664.

CADE-1994-Prehofer #decidability #higher-order #problem #unification

Decidable Higher-Order Unification Problems (CP), pp. 635–649.

CADE-1994-Salzer #unification

Primal Grammars and Unification Modulo a Binary Clause (GS), pp. 282–295.

CADE-1994-Socher-Ambrosius

A Refined Version of General E-Unification (RSA), pp. 665–677.

ICLP-1994-CairesM #higher-order #logic programming #polymorphism #unification

Higher-Order Polymorphic Unification for Logic Programming (LC, LM), pp. 419–433.

ILPS-1994-Marchiori #unification

Localizations of Unification Freedom through Matching Directions (MM), pp. 392–406.

ICALP-1993-Contejean #reduction

A Partial Solution for D-Unification Based on a Reduction to AC1-Unification (EC), pp. 621–632.

ICML-1993-Idestam-Almquist #anti #recursion

Generalization under Implication by Recursive Anti-unification (PIA), pp. 151–158.

ILPS-1993-Ait-KaciPG #order #unification

Order-Sorted Feature Theory Unification (HAK, AP, SCG), pp. 506–524.

ILPS-1993-KohlhaseP #unification #λ-calculus

Unification in a λ-Calculus with Intersection Types (MK, FP), pp. 488–505.

RTA-1993-Moser

Improving Transformation Systems for General E-Unification (MM), pp. 92–105.

ICALP-1992-FixFG #composition #unification

Program Composition via Unification (LF, NF, OG), pp. 672–684.

ML-1992-LapointeM #induction #named #performance #recursion #source code

Sub-unification: A Tool for Efficient Induction of Recursive Programs (SL, SM), pp. 273–281.

PLILP-1992-Holzbaur #unification

Metastructures versus Attributed Variables in the Context of Extensible Unification (CH), pp. 260–268.

CADE-1992-BaaderS #equation #unification

Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures (FB, KUS), pp. 50–65.

CADE-1992-BibelHW #unification

Cycle Unification (WB, SH, JW), pp. 94–108.

CADE-1992-Boudet #algebra #order #unification

Unification in Order-Sorted Algebras with Overloading (AB), pp. 193–207.

CADE-1992-DoughertyJ #approach #combinator #higher-order #logic

A Combinatory Logic Approach to Higher-order E-unification (Extended Abstract) (DJD, PJ), pp. 79–93.

CADE-1992-FrischC #unification

An Abstract View of Sorted Unification (AMF, AGC), pp. 178–192.

CADE-1992-NipkowQ #reduction #type system #unification #λ-calculus

Reduction and Unification in Lambda Calculi with Subtypes (TN, ZQ), pp. 66–78.

CADE-1992-Uribe #constraints #set #unification #using

Sorted Unification Using Set Constraints (TEU), pp. 163–177.

JICSLP-1992-Cerrito #calculus #ll #unification

Herbrand Methods in Sequent Calculi: Unification in LL (SC), pp. 607–621.

JICSLP-1992-ColussiM #unification

A Predicate Transformer for Unification (LC, EM), pp. 67–81.

JICSLP-1992-KirchnerR #algebra #algorithm #constraints #finite #theorem proving #unification

A Constraint Solver in Finite Algebras and Its Combination with Unification Algorithms (HK, CR), pp. 225–239.

JICSLP-1992-QianW #higher-order

Higher-Order E-Unification for Arbitrary Theories (ZQ, KW), pp. 52–66.

FPCA-1991-NipkowS #order #unification

Type Classes and Overloading Resolution via Order-Sorted Unification (TN, GS), pp. 1–14.

LOPSTR-1991-WaalG #algorithm #unification

Specialisation of a Unification Algorithm (DAdW, JPG), pp. 205–220.

ICLP-1991-CodishDY #algorithm #alias #analysis #safety #unification

Derivation and Safety of an Abstract Unification Algorithm for Groundness and Aliasing Analysis (MC, DD, EY), pp. 79–93.

ICLP-1991-Hagiya #higher-order #proving #theorem proving #unification

Higher-Order Unification as a Theorem Proving Procedure (MH), pp. 270–284.

ICLP-1991-Miller #logic programming #unification

Unification of Simply Typed Lamda-Terms as Logic Programming (DM), pp. 255–269.

ISLP-1991-MarienD #unification

A New Scheme for Unification in WAM (AM, BD), pp. 257–271.

LICS-1991-Pfenning #anti #calculus #unification

Unification and Anti-Unification in the Calculus of Constructions (FP), pp. 74–85.

RTA-1991-Baader #bound #problem #unification

Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems (FB), pp. 86–97.

RTA-1991-BaaderN #algebra #commutative #equation #how #morphism #unification

Adding Homomorphisms to Commutative/Monoidal Theories or How Algebra Can Help in Equational Unification (FB, WN), pp. 124–135.

RTA-1991-Domenjoud #order #unification

AC Unification Through Order-Sorted AC1 Unification (ED), pp. 98–111.

RTA-1991-NipkowQ #composition #higher-order

Modular Higher-Order E-Unification (TN, ZQ), pp. 200–214.

RTA-1991-Wolfram #equation #higher-order #unification

Rewriting, and Equational Unification: the Higher-Order Cases (DAW), pp. 25–36.

STOC-1990-KfouryTU #problem

The Undecidability of the Semi-Unification Problem (Preliminary Report) (AJK, JT, PU), pp. 468–476.

CADE-1990-Boudet #algorithm #equation #performance #unification

Unification in a Combination of Equational Theories: an Efficient Algorithm (AB), pp. 292–307.

CADE-1990-DoughertyJ

An Improved General E-Unification Method (DJD, PJ), pp. 261–275.

CADE-1990-Hagiya #higher-order #programming #proving #unification #using

Programming by Example and Proving by Example Using Higher-order Unification (MH), pp. 588–602.

CADE-1990-Kirchner #equation #tutorial #unification

Tutorial on Equational Unification (CK), p. 682.

CADE-1990-NarendranO #equation #unification

Some Results on Equational Unification (PN, FO), pp. 276–291.

CADE-1990-Nutt #unification

Unification in Monoidal Theories (WN), pp. 618–632.

CADE-1990-Snyder #higher-order

Higher Order E-Unification (WS), pp. 573–587.

CLP-1990-DelcherK90 #anti #parallel #performance

Efficient Parallel Term Matching and Anti-Unification (ALD, SK), pp. 355–369.

LICS-1990-BoudetCD #algorithm #equation #unification

A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations (AB, EC, HD), pp. 289–299.

LICS-1990-KirchnerK #unification

Syntactic Theories and Unification (CK, FK), pp. 270–277.

NACLP-1990-Umrigar #order #prolog #unification

Finding Advantageous Orders for Argument Unification for the Prolog WAM (ZDU), pp. 80–96.

FPCA-1989-RufW #functional #logic #nondeterminism #programming #unification

Nondeterminism and Unification in LogScheme: Integrating Logic and Functional Programming (ER, DW), pp. 327–339.

POPL-1989-KanellakisM #ml #polymorphism #type system #unification

Polymorphic Unification and ML Typing (PCK, JCM), pp. 105–115.

CSL-1989-Leiss #polymorphism #recursion

Polymorphic Recursion and Semi-Unification (HL), pp. 211–224.

LICS-1989-KfouryTU #problem #unification

Computational Consequences and Partial Solutions of a Generalized Unification Problem (Partial Report) (AJK, JT, PU), pp. 98–105.

NACLP-1989-Roy #prolog #unification

An Intermediate Language to Support Prolog’s Unification (PVR), pp. 1148–1164.

NACLP-1989-SinghalP #how #parallel #question #unification

Unification Parallelism: How Much Can We Exploit? (AS, YNP), pp. 1135–1147.

RTA-1989-Baader #unification

Characterization of Unification Type Zero (FB), pp. 2–14.

RTA-1989-DarlingtonG #abstraction #evaluation #functional #programming #set #unification

Narrowing and Unification in Functional Programming — An Evaluation Mechanism for Absolute Set Abstraction (JD, YG), pp. 92–108.

RTA-1989-Elliott #higher-order #unification

Higher-order Unification with Dependent Function Types (CE), pp. 121–136.

LFP-1988-Henglein #type inference

Type Inference and Semi-Unification (FH), pp. 184–197.

LFP-1988-Pfenning #higher-order #polymorphism #type inference #unification

Partial Polymorphic Type Inference and Higher-Order Unification (FP), pp. 153–163.

ALP-1988-Goltz #functional #modelling #semantics #unification

Functional Data Term Models and Semantic Unification (HJG), pp. 158–167.

CADE-1988-BlasiusS #equation #graph #reasoning #unification

Partial Unification for Graph Based Equational Reasoning (KHB, JHS), pp. 397–414.

CADE-1988-Buttner #algebra #finite #unification

Unification in Finite Algebras is Unitary (?) (WB), pp. 368–377.

CADE-1988-FranzenH #approach #unification

A New Approach to Universal Unification and Its Application to AC-Unification (MF, LJH), pp. 643–657.

CADE-1988-LincolnC #commutative #summary #unification

Adventures in Associative-Commutative Unification (A Summary) (PL, JC), pp. 358–367.

CADE-1988-Schmidt-Schauss #equation #unification

Unification in a Combination of Arbitrary Disjoint Equational Theories (MSS), pp. 378–396.

JICSCP-1988-AttilaF88 #evaluation #execution #semantics #source code

Unification-Free Execution of TYPOL Programs by Semantic Attribute Evaluation (IA, PFZ), pp. 160–177.

JICSCP-1988-HannanM88 #higher-order #implementation #unification

Uses of Higher-Order Unification for Implementing Program Transformers (JH, DM), pp. 942–959.

JICSCP-1988-JanssensDM88 #unification

Improving the Register Allocation of WAM by Recording Unification (GJ, BD, AM), pp. 1388–1402.

JICSCP-1988-Shankar88 #architecture #logic programming #memory management #unification

A Hierarchical Associative Memory Architecture for Logic Programming Unification (SS), pp. 1428–1447.

LICS-1988-BoudetJS #unification

Unification in Free Extensions of Boolean Rings and Abelian Groups (AB, JPJ, MSS), pp. 121–130.

LICS-1988-GallierSNP

Rigid E-Unification is NP-Complete (JHG, WS, PN, DAP), pp. 218–227.

LICS-1988-KuperMPP #algorithm #anti #parallel #performance

Efficient Parallel Algorithms for Anti-Unification and Relative Complement (GMK, KM, KVP, KJP), pp. 112–120.

ICALP-1987-Holldobler #algorithm #confluence #unification

A Unification Algorithms for Confluent Theories (SH), pp. 31–41.

CSL-1987-BlasiusH #unification

Resolution with Feature Unification (KHB, UH), pp. 17–26.

LICS-1987-GallierRS #equation #proving #theorem proving #using

Theorem Proving Using Rigid E-Unification Equational Matings (JHG, SR, WS), pp. 338–346.

RTA-1987-BurckertHS #decidability #equation #on the #unification

On Equational Theories, Unification and Decidability (HJB, AH, MSS), pp. 204–215.

RTA-1987-GallierS

A General Complete E-Unification Procedure (JHG, WS), pp. 216–227.

SLP-1987-ShinNHM87 #canonical #functional #logic #unification

A Functional Logic Language Based on Canonical Unification (DWS, JHN, SH, SM), pp. 328–334.

VLDB-1986-MoritaYNI #knowledge base #relational

Retrieval-By-Unification Operation on a Relational Knowledge Base (YM, HY, KN, HI), pp. 52–59.

ICALP-1986-YouS #algorithm #confluence #term rewriting

E-Unification Algorithms for a Class of Confluent Term Rewriting Systems (JHY, PAS), pp. 454–463.

GG-1986-Parisi-PresicceEM #composition #graph grammar #unification

Graph rewriting with unification and composition (FPP, HE, UM), pp. 496–514.

POPL-1986-JohnsonW #approach #incremental #type inference

A Maximum-Flow Approach to Anomaly Isolation in Unification-Based Incremental Type Inference (GFJ, JAW), pp. 44–57.

POPL-1986-SneltingH #algebra #analysis #incremental #semantics #unification

Unification in Many-Sorted Algebras as a Device for Incremental Semantic Analysis (GS, WH), pp. 229–235.

CADE-1986-Burckert #strict #unification

Some Relationships between Unification, restricted Unification, and Matching (HJB), pp. 514–524.

CADE-1986-Buttner #data type #set #unification

Unification in the Data Structure Sets (WB), pp. 470–488.

CADE-1986-Comon #anti #term rewriting

Sufficient Completeness, Term Rewriting Systems and “Anti-Unification” (HC), pp. 128–140.

CADE-1986-Herold #algorithm #unification

Combination of Unification Algorithms (AH), pp. 450–469.

CADE-1986-KapurN #problem #set #unification

NP-Completeness of the Set Unification and Matching Problems (DK, PN), pp. 489–495.

CADE-1986-MartinN #unification

Unification in Boolean Rings (UM, TN), pp. 506–513.

CADE-1986-Schmidt-Schauss #unification

Unification in Many-Sorted Eqational Theories (MSS), pp. 538–552.

CADE-1986-Tiden #set #unification

Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols (ET), pp. 431–449.

CADE-1986-Walther #classification #problem #unification

A Classification of Many-Sorted Unification Problems (CW), pp. 525–537.

ICLP-1986-MannilaU86 #complexity #on the #sequence #unification

On the Complexity of Unification Sequences (HM, EU), pp. 122–133.

LICS-1986-Kirchner #algorithm #unification

Computing Unification Algorithms (CK), pp. 206–216.

SLP-1986-GallierR86 #horn clause #similarity

SLD-Resolution Methods for Horn Clauses with Equality Based on E-Unification (JHG, SR), pp. 168–179.

SLP-1986-MartelliMR86 #algorithm #equation #unification

An Algorithm for Unification in Equational Theories (AM, CM, GR), pp. 180–186.

RTA-1985-ArnborgT #problem #unification

Unification Problems with One-Sided Distributivity (SA, ET), pp. 398–406.

RTA-1985-Fortenbach #algebra #commutative #unification

An Algebraic Approch to Unification Under Assoiativity and Commutativity (AF), pp. 381–397.

RTA-1985-Kandri-RodyKN #algebra #approach #commutative #problem #unification

An Ideal-Theoretic Approach to Work Problems and Unification Problems over Finitely Presented Commutative Algebras (AKR, DK, PN), pp. 345–364.

RTA-1985-RetyKKL #algorithm #logic programming #named #unification

NARROWER: A New Algorithm for Unification and Its Application to Logic Programming (PR, CK, HK, PL), pp. 141–157.

RTA-1985-Yelick #algorithm #equation #unification

Combining Unification Algorithms for Confined Regular Equational Theories (KAY), pp. 365–380.

SLP-1985-MaluszynskiK85 #execution #logic programming #source code

Unification-Free Execution of Logic Programs (JM, HJK), pp. 78–86.

POPL-1984-Bandes #programming language

Constraining-Unification and the Programming Language Unicorn (RGB), pp. 106–110.

CADE-1984-Fages #commutative #unification

Associative-Commutative Unification (FF), pp. 194–208.

CADE-1984-Kirchner #algorithm #equation #unification

A New Equational Unification Method: A Generalization of Martelli-Montanari’s Algorithm (CK), pp. 224–247.

CADE-1984-Siekmann #unification

Universal Unification (JHS), pp. 1–42.

ILPC-1984-Levy84 #algorithm #concurrent #prolog #unification

A Unification Algorithm for Concurrent Prolog (JL), pp. 333–341.

ILPC-1984-SabbatelDIN84 #database #prolog #unification

Unification for a Prolog Data Base Machine (GBS, WD, JCI, GTN), pp. 207–217.

ICALP-1983-JouannaudKK #algorithm #equation #incremental #unification

Incremental Construction of Unification Algorithms in Equational Theories (JPJ, CK, HK), pp. 361–373.

POPL-1983-Wegner #abstraction #ada #on the #unification

On the Unification of Data and Program Abstraction in Ada (PW), pp. 256–264.

CADE-1982-SiekmannS #classification #equation #unification

Universal Unification and a Classification of Equational Theories (JHS, PS), pp. 369–389.

ILPC-1982-Abramson82

Unification-based Conditional Binding Constructs (HA), pp. 182–186.

CADE-1980-Hullot #canonical #unification

Canonical Forms and Unification (JMH), pp. 318–334.

STOC-1976-PatersonW #linear #unification

Linear Unification (MP, MNW), pp. 181–186.