BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
unification
Google unification

Tag #unification

230 papers:

CSLCSL-2020-Jez #equation #problem #word
Solving Word Equations (And Other Unification Problems) by Recompression (Invited Talk) (AJ), p. 17.
DLTDLT-2019-Jez #constraints
Deciding Context Unification (with Regular Constraints) (AJ), pp. 18–40.
FMFM-2019-ArusoaieL #logic
Unification in Matching Logic (AA, DL), pp. 502–518.
CADECADE-2019-AnantharamanHNR #equation #word
Unification Modulo Lists with Reverse Relation with Certain Word Equations (SA, PH, PN, MR), pp. 1–17.
CADECADE-2019-BhayatR #combinator #strict
Restricted Combinatory Unification (AB, GR), pp. 74–93.
FSCDFSCD-2018-Ayala-RinconFN #constraints #equation #fixpoint
Fixed-Point Constraints for Nominal Equational Unification (MAR, MF, DNS), p. 16.
FSCDFSCD-2018-Schmidt-Schauss
Nominal Unification with Atom and Context Variables (MSS, DS), p. 20.
GPCEGPCE-2018-StuckiBO #metaprogramming #multi
A practical unification of multi-stage programming and macros (NS, AB, MO), pp. 14–27.
MSRMSR-2017-HurierSDBTKC #android #anti #named
Euphony: harmonious unification of cacophonous anti-virus vendor labels for Android malware (MH, GST, SKD, TFB, YLT, JK, LC), pp. 425–435.
LOPSTRLOPSTR-2017-Ait-KaciP #first-order #fuzzy
Fuzzy Unification and Generalization of First-Order Terms over Similar Signatures (HAK, GP), pp. 218–234.
PPDPPPDP-2017-MesnardPV #constraints #logic programming
Selective unification in constraint logic programming (FM, ÉP, GV), pp. 115–126.
FSCDFSCD-2016-DudenhefnerMR #problem
The Intersection Type Unification Problem (AD, MM, JR), p. 16.
FSCDFSCD-2016-LibalM #higher-order
Functions-as-Constructors Higher-Order Unification (TL, DM0), p. 17.
ICFP-2016-CockxDP
Unifiers as equivalences: proof-relevant unification of dependently typed data (JC, DD, FP), pp. 270–283.
MoDELSMoDELS-2016-BatotS #framework #learning #testing
A generic framework for model-set selection for the unification of testing and learning MDE tasks (EB, HAS), pp. 374–384.
LOPSTRLOPSTR-2016-MesnardPV #logic programming #on the #source code #testing
On the Completeness of Selective Unification in Concolic Testing of Logic Programs (FM, ÉP, GV), pp. 205–221.
LOPSTRLOPSTR-2016-Schmidt-Schauss #higher-order #recursion
Nominal Unification of Higher Order Expressions with Recursive Let (MSS, TK, JL, MV), pp. 328–344.
PPDPPPDP-2016-Schmidt-Schauss #recursion
Unification of program expressions with recursive bindings (MSS, DS), pp. 160–173.
IJCARIJCAR-2016-DuranEEMMT #generative #maude
Built-in Variant Generation and Unification, and Their Applications in Maude 2.7 (FD, SE, SE, NMO, JM, CLT), pp. 183–192.
RTARTA-2015-KotsireasKS #design #equation #orthogonal
Constructing Orthogonal Designs in Powers of Two: Gröbner Bases Meet Equational Unification (ISK, TK, DES), pp. 241–256.
ICFPICFP-2015-ZilianiS #algorithm #coq #morphism #polymorphism
A unification algorithm for Coq featuring universe polymorphism and overloading (BZ, MS), pp. 179–191.
CADECADE-2015-Libal #higher-order
Regular Patterns in Second-Order Unification (TL), pp. 557–571.
CAVCAV-2015-AlurCR #synthesis
Synthesis Through Unification (RA, PC, AR), pp. 163–179.
CSLCSL-2015-GasconST #polynomial #strict
Two-Restricted One Context Unification is in Polynomial Time (AG, MSS, AT), pp. 405–422.
LICSLICS-2015-GasconTS #polynomial #problem
One Context Unification Problems Solvable in Polynomial Time (AG, AT, MSS), pp. 499–510.
SANERCSMR-WCRE-2014-KrishnanT #refactoring
Unification and refactoring of clones (GPK, NT), pp. 104–113.
ICALPICALP-v2-2014-Jez
Context Unification is in PSPACE (AJ), pp. 244–255.
RTARTA-TLCA-2014-AubertB
Unification and Logarithmic Space (CA, MB), pp. 77–92.
PPDPPPDP-2014-YangEMMN #encryption #finite
Theories of Homomorphic Encryption, Unification, and the Finite Variant Property (FY, SE, CM, JM, PN), pp. 123–133.
FoSSaCSFoSSaCS-2014-ErbaturKMMNR #on the #problem #symmetry
On Asymmetric Unification and the Combination Problem in Disjoint Theories (SE, DK, AMM, CM, PN, CR), pp. 274–288.
RTARTA-2013-Calves
Unifying Nominal Unification (CC), pp. 143–157.
RTARTA-2013-SmolkaT #recursion
Unification Modulo Nonnested Recursion Schemes via Anchored Semi-Unification (GS, TT), pp. 271–286.
KDIRKDIR-KMIS-2013-SaidiDZC #process #requirements #semantics #towards #using
Towards Unification of Requirements Engineering Approaches using Semantics-based Process (IES, TD, NZ, PJC), pp. 443–450.
CADECADE-2013-ErbaturEKLLMMNSS #analysis #encryption #paradigm #protocol #symmetry
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis (SE, SE, DK, ZL, CL, CM, JM, PN, SS, RS), pp. 231–248.
LATALATA-2012-AnantharamanBNR
Unification Modulo Chaining (SA, CB, PN, MR), pp. 70–82.
RTARTA-2012-CreusGG
One-context Unification with STG-Compressed Terms is in NP (CC, AG, GG), pp. 149–164.
KRKR-2012-BaaderBM #towards
Extending Unification in EL Towards General TBoxes (FB, SB, BM).
ECMFAECMFA-2012-VarroAS #pattern matching
Unification of Compiled and Interpreter-Based Pattern Matching Techniques (GV, AA, AS), pp. 368–383.
ICLPICLP-2012-BryS #query #semistructured data #simulation
Simulation Unification: Beyond Querying Semistructured Data (FB, SS), pp. 1–13.
IJCARIJCAR-2012-AnantharamanELNR
Unification Modulo Synchronous Distributivity (SA, SE, CL, PN, MR), pp. 14–29.
IJCARIJCAR-2012-BaaderBM #encoding #ontology #satisfiability #strict
SAT Encoding of Unification in ℰℒℋ_R⁺ w.r.t. Cycle-Restricted Ontologies (FB, SB, BM), pp. 30–44.
IJCARIJCAR-2012-BaaderMM #logic #named
UEL: Unification Solver for the Description Logic ℰℒ — System Description (FB, JM, BM), pp. 45–51.
IJCARIJCAR-2012-MarshallN #algorithm
New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants (AMM, PN), pp. 408–422.
ITiCSEITiCSE-2011-GarciaMGH #interface #learning
A system for usable unification of interfaces of learning objects in m-learning (EG, LdM, AGC, JRH), p. 347.
RTARTA-2011-DuranEEMT #maude #reachability
Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6 (FD, SE, SE, JM, CLT), pp. 31–40.
RTARTA-2011-GasconMR #first-order
First-Order Unification on Compressed Terms (AG, SM, LR), pp. 51–60.
TLCATLCA-2011-AbelP #dependent type #higher-order
Higher-Order Dynamic Pattern Unification for Dependent Types and Records (AA, BP), pp. 10–26.
ICEISICEIS-v1-2011-MessaoudFKZ #documentation #xml
Unification of XML Document Structures for Document Warehouse (DocW) (IBM, JF, KK, GZ), pp. 85–94.
PPDPPPDP-2011-EscobarKLMMNS #analysis #encryption #protocol #using
Protocol analysis in Maude-NPA using unification modulo homomorphic encryption (SE, DK, CL, CM, JM, PN, RS), pp. 65–76.
SACSAC-2011-Jamil #graph #query #using
Computing subgraph isomorphic queries using structural unification and minimum graph structures (HMJ), pp. 1053–1058.
CADECADE-2011-BaaderBBM #concept #logic
Unification in the Description Logic EL without the Top Concept (FB, TBN, SB, BM), pp. 70–84.
CADECADE-2011-LiuL #morphism #performance
Efficient General Unification for XOR with Homomorphism (ZL, CL), pp. 407–421.
RTARTA-2010-KutsiaM #order #regular expression
Order-Sorted Unification with Regular Expression Sorts (TK, MM), pp. 193–208.
RTARTA-2010-LevyV #algorithm #performance
An Efficient Nominal Unification Algorithm (JL, MV), pp. 209–226.
FMFM-2009-Boute #logic
Making Temporal Logic Calculational: A Tool for Unification and Discovery (RTB), pp. 387–402.
RTARTA-2009-BaaderM #logic
Unification in the Description Logic EL (FB, BM), pp. 350–364.
RTARTA-2009-ClavelDEELMMT #maude
Unification and Narrowing in Maude 2.4 (MC, FD, SE, SE, PL, NMO, JM, CLT), pp. 380–390.
RTARTA-2009-GasconGS
Unification with Singleton Tree Grammars (AG, GG, MSS), pp. 365–379.
WRLAWRLA-2008-EscobarMS09 #equation
Variant Narrowing and Equational Unification (SE, JM, RS), pp. 103–119.
TPDLECDL-2008-DoganS #physics
Virtual Unification of the Earliest Christian Bible: Digitisation, Transcription, Translation and Physical Description of the Codex Sinaiticus (ZMD, AS), pp. 221–226.
ICALPICALP-A-2008-AzarG #framework #integer #source code
Truthful Unification Framework for Packing Integer Programs with Choices (YA, IG), pp. 833–844.
RTARTA-2008-LevyV #higher-order #perspective
Nominal Unification from a Higher-Order Perspective (JL, MV), pp. 246–260.
PADLPADL-2008-CoxN #array #logic programming #spreadsheet
Unification of Arrays in Spreadsheets with Logic Programming (PTC, PKN), pp. 100–115.
IJCARIJCAR-2008-TourEN #equation
Unification and Matching Modulo Leaf-Permutative Equational Presentations (TBdlT, ME, PN), pp. 332–347.
RTARTA-2007-KutsiaLV #sequence
Sequence Unification Through Currying (TK, JL, MV), pp. 288–302.
LOPSTRLOPSTR-2007-ZhangN #constraints #scalability #theorem proving #using
A Scalable Inclusion Constraint Solver Using Unification (YZ, FN), pp. 121–137.
SACSAC-2007-DjelloulDF #constraints #finite #first-order #infinity #prolog #theorem proving #towards #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.
RTARTA-2006-LevySV #bound #higher-order
Bounded Second-Order Unification Is NP-Complete (JL, MSS, MV), pp. 400–414.
IJCARIJCAR-2006-LevySV
Stratified Context Unification Is NP-Complete (JL, MSS, MV), pp. 82–96.
IJCARIJCAR-2006-Pientka #approach #higher-order #lightweight
Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach (BP), pp. 362–376.
RTARTA-2005-Cheney
Equivariant Unification (JC), pp. 74–89.
RTARTA-2005-TourE
Unification in a Class of Permutative Theories (TBdlT, ME), pp. 105–119.
DiGRADiGRA-2005-Arbiser #concept #game studies #towards
Towards the unification of intuitive and formal game concepts with applications to computer chess (AA).
SEKESEKE-2005-BasitRJ #empirical #using
An Empirical Study on Limits of Clone Unification Using Generics (HAB, DCR, SJ), pp. 109–114.
PPDPPPDP-2005-LiL
Inverting abstract unification for set-sharing (XL, LL), pp. 129–138.
CADECADE-2005-LevyNV
Well-Nested Context Unification (JL, JN, MV), pp. 149–163.
ICLPICLP-2005-NadathurL #higher-order #on the fly
Practical Higher-Order Pattern Unification with On-the-Fly Raising (GN, NL), pp. 371–386.
ICALPICALP-2004-Cheney #complexity
The Complexity of Equivariant Unification (JC), pp. 332–344.
RTARTA-2004-LevySV #higher-order #monad
Monadic Second-Order Unification Is NP-Complete (JL, MSS, MV), pp. 55–69.
RTARTA-2004-MitsuhashiOOY #confluence #problem
The Joinability and Unification Problems for Confluent Semi-constructor TRSs (IM, MO, YO, TY), pp. 285–300.
ICPRICPR-v2-2004-YinFD #framework
A Unification Framework for Tree and Block Wavelet Encoders (XWY, MF, ACD), pp. 795–798.
GPCEGPCE-2004-Schultz #automation #inheritance
A Unification of Inheritance and Automatic Program Specialization (UPS), pp. 244–265.
EDOCEDOC-2003-BurtBROA #data access #modelling #security
Model Driven Security: Unification of Authorization Models for Fine-Grain Access Control (CCB, BRB, RRR, AMO, MA), pp. 159–173.
SIGIRSIGIR-2003-Davison #analysis #towards
Toward a unification of text and link analysis (BDD0), pp. 367–368.
CADECADE-2003-AnantharamanNR #morphism
Unification Modulo ACU I Plus Homomorphisms/Distributivity (SA, PN, MR), pp. 442–457.
CADECADE-2003-ChoppellaH
Source-Tracking Unification (VC, CTH), pp. 458–472.
CADECADE-2003-Lynch #problem
Schematic Saturation for Decision and Unification Problems (CL), pp. 427–441.
CADECADE-2003-PientkaP #higher-order #optimisation
Optimizing Higher-Order Pattern Unification (BP, FP), pp. 473–487.
RTARTA-2002-LevyV #higher-order #problem
Currying Second-Order Unification Problems (JL, MV), pp. 326–339.
ICPRICPR-v3-2002-TanCM #image #named #retrieval #towards
SmartAlbum — Towards Unification of Approaches for Image Retrieval (TT, JC, PM), pp. 983–986.
CSLCSL-2002-Schmidt-SchaussS #bound #decidability #higher-order
Decidability of Bounded Higher-Order Unification (MSS, KUS), pp. 522–536.
ICLPICLP-2002-BryS #declarative #model transformation #query #semistructured data #simulation #towards #transformation language #xml
Towards a Declarative Query and Transformation Language for XML and Semistructured Data: Simulation Unification (FB, SS), pp. 255–270.
RTARTA-2001-LevyV #equation #traversal
Context Unification and Traversal Equations (JL, MV), pp. 169–184.
RTARTA-2001-OyamaguchiO #confluence #problem #term rewriting
The Unification Problem for Confluent Right-Ground Term Rewriting Systems (MO, YO), pp. 246–260.
ICFPICFP-2001-Sheard
Generic Unification via Two-Level Types and Parameterized Modules (TS), pp. 86–97.
SACSAC-2001-Jamil #relational
A case for parameterized views and relational unification (HMJ), pp. 275–279.
CCCC-2001-KandemirU #array #locality #optimisation
Array Unification: A Locality Optimization Technique (MTK), pp. 259–273.
CSLCSL-2001-Schmidt-Schauss
Stratified Context Unification Is in PSPACE (MSS), pp. 498–512.
RTARTA-2000-BjornerM
Absolute Explicit Unification (NB, CM), pp. 31–46.
RTARTA-2000-LevyV #constraints #higher-order #linear
Linear Second-Order Unification and Context Unification with Tree-Regular Constraints (JL, MV), pp. 156–171.
PPDPPPDP-2000-Ayala-RinconK
Unification via se-style of explicit substitution (MAR, FK), pp. 163–174.
CADECADE-2000-Sofronie-Stokkermans #on the
On Unification for Bonded Distributive Lattices (VSS), pp. 465–481.
RTARTA-1999-KepserR #algorithm #equation #named
UNIMOK: A System for Combining Equational Unification Algorithm (SK, JR), pp. 248–251.
ICMLICML-1999-UtgoffS #approximate
Approximation Via Value Unification (PEU, DJS), pp. 425–432.
FoSSaCSFoSSaCS-1999-DantsinV #algorithm #nondeterminism #polynomial #set
A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees (ED, AV), pp. 180–196.
RTARTA-1998-GuoNS #algebra #process
Unification and Matching in Process Algebras (QG, PN, SKS), pp. 91–105.
RTARTA-1998-JacquemardMW #equation
Unification in Extension of Shallow Equational Theories (FJ, CM, CW), pp. 76–90.
RTARTA-1998-Levy #decidability #higher-order #problem
Decidable and Undecidable Second-Order Unification Problems (JL), pp. 47–60.
IFLIFL-1998-McAdam #interface #on the
On the Unification of Substitutions in Type Interfaces (BJM), pp. 137–152.
POPLPOPL-1998-Schubert #higher-order #morphism #polymorphism #type inference
Second-Order Unification and Type Inference for Church-Style Polymorphism (AS), pp. 279–288.
CADECADE-1998-Beeson #λ-calculus
Unification in Lambda-Calculi with if-then-else (MB), pp. 103–118.
LICSLICS-1998-Veanes #higher-order
The Relation Between Second-Order Unification and Simultaneous Rigid E-Unification (MV), pp. 264–275.
RTARTA-1997-Ringeissen #algorithm #programming language #prototype #rule-based
Prototyping Combination of Unification Algorithms with the ELAN Rule-Based Programming Language (CR), pp. 323–326.
TOOLSTOOLS-USA-1997-AllenHF #uml
Method Unification: UML and OML (RA, BHS, DF), p. 372.
PPDPALP-1997-KirchnerR #equation #higher-order
Higher-Order Equational Unification via Explicit Substitutions (CK, CR), pp. 61–75.
DACDAC-1997-SarrafzadehKT
Unification of Budgeting and Placement (MS, DAK, GET), pp. 758–761.
CADECADE-1997-NiehrenPR #constraints #finite #on the #similarity
On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting (JN, MP, PR), pp. 34–48.
ICLPICLP-1997-AjiliK #composition #constraints #framework
A Modular Framework for the Combination of Unification and Built-In Constraints (FA, CK), pp. 331–345.
LICSLICS-1997-Goubault-Larrecq #higher-order
Ramified Higher-Order Unification (JGL), pp. 410–421.
RTARTA-1996-BoudetCM #proving #theorem proving
AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.
RTARTA-1996-FettigL #finite #higher-order #λ-calculus
Unification of Higher-Order patterns in a Simply Typed λ-Calculus with Finite Products and terminal Type (RF, BL), pp. 347–361.
RTARTA-1996-Levy #higher-order #linear
Linear Second-Order Unification (JL), pp. 332–346.
RTARTA-1996-Schmidt-Schauss #algorithm
An Algorithm for Distributive Unification (MSS), pp. 287–301.
CAiSECAiSE-1996-CastanoA #analysis #process
Techniques for Process Analysis and Unification (SC, VDA), pp. 234–254.
CIKMCIKM-1996-Greco #bound #set
Optimal Unification of Bounded Simple Set Terms (SG), pp. 326–336.
CADECADE-1996-GuoNW
Unification and Matching Modulo Nilpotence (QG, PN, DAW), pp. 261–274.
CADECADE-1996-HermannK #algorithm #polynomial
Unification Algorithms Cannot be Combined in Polynomial Time (MH, PGK), pp. 246–260.
CADECADE-1996-Weidenbach #decidability #pseudo
Unification in Pseudo-Linear Sort Theories is Decidable (CW), pp. 343–357.
ICLPJICSLP-1996-DowekHKP #higher-order
Unification via Explicit Substitutions: The Case of Higher-Order Patterns (GD, TH, CK, FP), pp. 259–273.
RTARTA-1995-OttoND #equation #independence
Some Independent Results for Equational Unification (FO, PN, DJD), pp. 367–381.
LOPSTRLOPSTR-1995-ArtsZ #logic programming #semantics #source code #termination #using
Termination of Logic Programs Using Semantic Unification (TA, HZ), pp. 219–233.
PPDPPLILP-1995-Arenas-SanchezD #set
Minimal Set Unification (PAS, AD), pp. 397–414.
POPLPOPL-1995-DawsonRRSSSW #execution #logic programming #performance #source code
Unification Factoring for Efficient Execution of Logic Programs (SD, CRR, IVR, KFS, SS, TS, DSW), pp. 247–258.
ICLPILPS-1995-DawsonRRS #optimisation
Optimizing Clause Resolution: Beyond Unification Factoring (SD, CRR, IVR, TS), pp. 194–208.
LICSLICS-1995-DowekHK #higher-order
Higher-Order Unification via Explicit Substitutions (GD, TH, CK), pp. 366–374.
ICGTTAGT-1994-PlumpH #graph
Graph Unification and Matching (DP, AH), pp. 75–88.
SACSAC-1994-LiB #object-oriented #parsing
An integrated parsing scheme for unification categorial grammar with object-oriented lexicon (LL, BRB), pp. 524–528.
PDPPDP-1994-CiampoliniLMS #architecture #parallel
Multi-level Copying For Unification In Parallel Architectures (AC, EL, PM, CS), pp. 518–525.
ESOPESOP-1994-Hanus #lazy evaluation
Lazy Unification with Simplification (MH), pp. 272–286.
CADECADE-1994-JohannK #constant #order #λ-calculus
Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading (PJ, MK), pp. 620–634.
CADECADE-1994-Prehofer #decidability #higher-order #problem
Decidable Higher-Order Unification Problems (CP), pp. 635–649.
CADECADE-1994-Salzer
Primal Grammars and Unification Modulo a Binary Clause (GS), pp. 282–295.
ICLPICLP-1994-CairesM #higher-order #logic programming #polymorphism
Higher-Order Polymorphic Unification for Logic Programming (LC, LM), pp. 419–433.
ICLPILPS-1994-Marchiori
Localizations of Unification Freedom through Matching Directions (MM), pp. 392–406.
TAPSOFTTAPSOFT-1993-Qian #higher-order #linear
Linear Unification of Higher-Order Patterns (ZQ), pp. 391–405.
ICLPILPS-1993-Ait-KaciPG #order
Order-Sorted Feature Theory Unification (HAK, AP, SCG), pp. 506–524.
ICLPILPS-1993-KohlhaseP #λ-calculus
Unification in a λ-Calculus with Intersection Types (MK, FP), pp. 488–505.
ICALPICALP-1992-FixFG #composition
Program Composition via Unification (LF, NF, OG), pp. 672–684.
PPDPPLILP-1992-Holzbaur
Metastructures versus Attributed Variables in the Context of Extensible Unification (CH), pp. 260–268.
CADECADE-1992-BaaderS #equation
Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures (FB, KUS), pp. 50–65.
CADECADE-1992-BibelHW
Cycle Unification (WB, SH, JW), pp. 94–108.
CADECADE-1992-Boudet #algebra #order
Unification in Order-Sorted Algebras with Overloading (AB), pp. 193–207.
CADECADE-1992-FrischC
An Abstract View of Sorted Unification (AMF, AGC), pp. 178–192.
CADECADE-1992-NipkowQ #reduction #type system #λ-calculus
Reduction and Unification in Lambda Calculi with Subtypes (TN, ZQ), pp. 66–78.
CADECADE-1992-Uribe #constraints #set #using
Sorted Unification Using Set Constraints (TEU), pp. 163–177.
ICLPJICSLP-1992-Cerrito #calculus #ll
Herbrand Methods in Sequent Calculi: Unification in LL (SC), pp. 607–621.
ICLPJICSLP-1992-ColussiM
A Predicate Transformer for Unification (LC, EM), pp. 67–81.
ICLPJICSLP-1992-KirchnerR #algebra #algorithm #constraints #finite #theorem proving
A Constraint Solver in Finite Algebras and Its Combination with Unification Algorithms (HK, CR), pp. 225–239.
RTARTA-1991-Baader #bound #problem
Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems (FB), pp. 86–97.
RTARTA-1991-BaaderN #algebra #commutative #equation #how #morphism
Adding Homomorphisms to Commutative/Monoidal Theories or How Algebra Can Help in Equational Unification (FB, WN), pp. 124–135.
RTARTA-1991-Domenjoud #order
AC Unification Through Order-Sorted AC1 Unification (ED), pp. 98–111.
RTARTA-1991-Wolfram #equation #higher-order
Rewriting, and Equational Unification: the Higher-Order Cases (DAW), pp. 25–36.
FPCAFPCA-1991-NipkowS #order
Type Classes and Overloading Resolution via Order-Sorted Unification (TN, GS), pp. 1–14.
LOPSTRLOPSTR-1991-WaalG #algorithm
Specialisation of a Unification Algorithm (DAdW, JPG), pp. 205–220.
ICLPICLP-1991-CodishDY #algorithm #alias #analysis #safety
Derivation and Safety of an Abstract Unification Algorithm for Groundness and Aliasing Analysis (MC, DD, EY), pp. 79–93.
ICLPICLP-1991-Hagiya #higher-order #proving #theorem proving
Higher-Order Unification as a Theorem Proving Procedure (MH), pp. 270–284.
ICLPICLP-1991-Miller #logic programming
Unification of Simply Typed Lamda-Terms as Logic Programming (DM), pp. 255–269.
ICLPISLP-1991-MarienD
A New Scheme for Unification in WAM (AM, BD), pp. 257–271.
LICSLICS-1991-Pfenning #anti #calculus
Unification and Anti-Unification in the Calculus of Constructions (FP), pp. 74–85.
CADECADE-1990-Boudet #algorithm #equation #performance
Unification in a Combination of Equational Theories: an Efficient Algorithm (AB), pp. 292–307.
CADECADE-1990-Hagiya #higher-order #programming #proving #using
Programming by Example and Proving by Example Using Higher-order Unification (MH), pp. 588–602.
CADECADE-1990-Kirchner #equation #tutorial
Tutorial on Equational Unification (CK), p. 682.
CADECADE-1990-NarendranO #equation
Some Results on Equational Unification (PN, FO), pp. 276–291.
CADECADE-1990-Nutt
Unification in Monoidal Theories (WN), pp. 618–632.
LICSLICS-1990-BoudetCD #algorithm #equation
A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations (AB, EC, HD), pp. 289–299.
LICSLICS-1990-KirchnerK
Syntactic Theories and Unification (CK, FK), pp. 270–277.
ICLPNACLP-1990-Umrigar #order #prolog
Finding Advantageous Orders for Argument Unification for the Prolog WAM (ZDU), pp. 80–96.
RTARTA-1989-Baader
Characterization of Unification Type Zero (FB), pp. 2–14.
RTARTA-1989-DarlingtonG #abstraction #evaluation #functional #programming #set
Narrowing and Unification in Functional Programming — An Evaluation Mechanism for Absolute Set Abstraction (JD, YG), pp. 92–108.
RTARTA-1989-Elliott #higher-order
Higher-order Unification with Dependent Function Types (CE), pp. 121–136.
FPCAFPCA-1989-RufW #functional #logic #nondeterminism #programming
Nondeterminism and Unification in LogScheme: Integrating Logic and Functional Programming (ER, DW), pp. 327–339.
POPLPOPL-1989-KanellakisM #ml #polymorphism #type system
Polymorphic Unification and ML Typing (PCK, JCM), pp. 105–115.
LICSLICS-1989-KfouryTU #problem
Computational Consequences and Partial Solutions of a Generalized Unification Problem (AJK, JT, PU), pp. 98–105.
ICLPNACLP-1989-Roy #prolog
An Intermediate Language to Support Prolog’s Unification (PVR), pp. 1148–1164.
ICLPNACLP-1989-SinghalP #how #parallel #question
Unification Parallelism: How Much Can We Exploit? (AS, YNP), pp. 1135–1147.
LISPLFP-1988-Pfenning #higher-order #polymorphism #type inference
Partial Polymorphic Type Inference and Higher-Order Unification (FP), pp. 153–163.
PPDPALP-1988-Goltz #functional #modelling #semantics
Functional Data Term Models and Semantic Unification (HJG), pp. 158–167.
CADECADE-1988-BlasiusS #equation #graph #reasoning
Partial Unification for Graph Based Equational Reasoning (KHB, JHS), pp. 397–414.
CADECADE-1988-Buttner #algebra #finite
Unification in Finite Algebras is Unitary (?) (WB), pp. 368–377.
CADECADE-1988-FranzenH #approach
A New Approach to Universal Unification and Its Application to AC-Unification (MF, LJH), pp. 643–657.
CADECADE-1988-LincolnC #commutative
Adventures in Associative-Commutative Unification (PL, JC), pp. 358–367.
CADECADE-1988-Schmidt-Schauss #equation
Unification in a Combination of Arbitrary Disjoint Equational Theories (MSS), pp. 378–396.
ICLPJICSCP-1988-HannanM88 #higher-order #implementation
Uses of Higher-Order Unification for Implementing Program Transformers (JH, DM), pp. 942–959.
ICLPJICSCP-1988-JanssensDM88
Improving the Register Allocation of WAM by Recording Unification (GJ, BD, AM), pp. 1388–1402.
ICLPJICSCP-1988-Shankar88 #architecture #logic programming #memory management
A Hierarchical Associative Memory Architecture for Logic Programming Unification (SS), pp. 1428–1447.
LICSLICS-1988-BoudetJS
Unification in Free Extensions of Boolean Rings and Abelian Groups (AB, JPJ, MSS), pp. 121–130.
ICALPICALP-1987-Holldobler #algorithm #confluence
A Unification Algorithms for Confluent Theories (SH), pp. 31–41.
RTARTA-1987-BurckertHS #decidability #equation #on the
On Equational Theories, Unification and Decidability (HJB, AH, MSS), pp. 204–215.
TAPSOFTCAAP-1987-Rocca
An Unification Semi-Algorithm for Intersection Type Schemes (SRDR), pp. 37–51.
TAPSOFTCFLP-1987-BoscoGM #semantics
Refined Strategies for Semantic Unification (PGB, EG, CM), pp. 276–290.
CSLCSL-1987-BlasiusH
Resolution with Feature Unification (KHB, UH), pp. 17–26.
ICLPSLP-1987-ShinNHM87 #canonical #functional #logic
A Functional Logic Language Based on Canonical Unification (DWS, JHN, SH, SM), pp. 328–334.
ICGTGG-1986-Parisi-PresicceEM #composition #graph grammar
Graph rewriting with unification and composition (FPP, HE, UM), pp. 496–514.
POPLPOPL-1986-SneltingH #algebra #analysis #incremental #semantics
Unification in Many-Sorted Algebras as a Device for Incremental Semantic Analysis (GS, WH), pp. 229–235.
CADECADE-1986-Burckert #strict
Some Relationships between Unification, restricted Unification, and Matching (HJB), pp. 514–524.
CADECADE-1986-Buttner #data type #set
Unification in the Data Structure Sets (WB), pp. 470–488.
CADECADE-1986-Herold #algorithm
Combination of Unification Algorithms (AH), pp. 450–469.
CADECADE-1986-KapurN #problem #set
NP-Completeness of the Set Unification and Matching Problems (DK, PN), pp. 489–495.
CADECADE-1986-MartinN
Unification in Boolean Rings (UM, TN), pp. 506–513.
CADECADE-1986-Schmidt-Schauss
Unification in Many-Sorted Eqational Theories (MSS), pp. 538–552.
CADECADE-1986-Tiden #set
Unification in Combinations of Collapse-Free Theories with Disjoint Sets of Function Symbols (ET), pp. 431–449.
CADECADE-1986-Walther #classification #problem
A Classification of Many-Sorted Unification Problems (CW), pp. 525–537.
ICLPICLP-1986-MannilaU86 #complexity #on the #sequence
On the Complexity of Unification Sequences (HM, EU), pp. 122–133.
LICSLICS-1986-Kirchner #algorithm
Computing Unification Algorithms (CK), pp. 206–216.
ICLPSLP-1986-MartelliMR86 #algorithm #equation
An Algorithm for Unification in Equational Theories (AM, CM, GR), pp. 180–186.
RTARTA-1985-ArnborgT #problem
Unification Problems with One-Sided Distributivity (SA, ET), pp. 398–406.
RTARTA-1985-Fortenbach #algebra #commutative
An Algebraic Approch to Unification Under Assoiativity and Commutativity (AF), pp. 381–397.
RTARTA-1985-Kandri-RodyKN #algebra #approach #commutative #problem
An Ideal-Theoretic Approach to Work Problems and Unification Problems over Finitely Presented Commutative Algebras (AKR, DK, PN), pp. 345–364.
RTARTA-1985-RetyKKL #algorithm #logic programming #named
NARROWER: A New Algorithm for Unification and Its Application to Logic Programming (PR, CK, HK, PL), pp. 141–157.
RTARTA-1985-Yelick #algorithm #equation
Combining Unification Algorithms for Confined Regular Equational Theories (KAY), pp. 365–380.
CADECADE-1984-Fages #commutative
Associative-Commutative Unification (FF), pp. 194–208.
CADECADE-1984-Kirchner #algorithm #equation
A New Equational Unification Method: A Generalization of Martelli-Montanari’s Algorithm (CK), pp. 224–247.
CADECADE-1984-Siekmann
Universal Unification (JHS), pp. 1–42.
ICLPILPC-1984-Levy84 #algorithm #concurrent #prolog
A Unification Algorithm for Concurrent Prolog (JL), pp. 333–341.
ICLPILPC-1984-SabbatelDIN84 #database #prolog
Unification for a Prolog Data Base Machine (GBS, WD, JCI, GTN), pp. 207–217.
ICALPICALP-1983-JouannaudKK #algorithm #equation #incremental
Incremental Construction of Unification Algorithms in Equational Theories (JPJ, CK, HK), pp. 361–373.
POPLPOPL-1983-Wegner #abstraction #ada #on the
On the Unification of Data and Program Abstraction in Ada (PW), pp. 256–264.
CADECADE-1982-SiekmannS #classification #equation
Universal Unification and a Classification of Equational Theories (JHS, PS), pp. 369–389.
CADECADE-1980-Hullot #canonical
Canonical Forms and Unification (JMH), pp. 318–334.
STOCSTOC-1976-PatersonW #linear
Linear Unification (MP, MNW), pp. 181–186.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.