Refine
Year of publication
Document Type
- Working Paper (89)
- Conference Proceeding (4)
- Article (3)
Language
- English (96)
Has Fulltext
- yes (96)
Is part of the Bibliography
- no (96)
Keywords
- Lambda-Kalkül (17)
- Formale Semantik (9)
- Operationale Semantik (8)
- lambda calculus (8)
- Programmiersprache (7)
- concurrency (6)
- functional programming (6)
- Nebenläufigkeit (5)
- pi-calculus (5)
- semantics (5)
- Logik (4)
- Verifikation (4)
- adequate translations (4)
- contextual equivalence (4)
- letrec (4)
- automated deduction (3)
- call-by-need (3)
- context lemma (3)
- functional programming languages (3)
- observational semantics (3)
- Funktionale Programmiersprache (2)
- Funktionale Programmierung (2)
- Kontextuelle Gleichheit (2)
- Logics (2)
- Programmtransformation (2)
- Pufferspeicher (2)
- Semantics (2)
- Verification (2)
- call-by-name (2)
- context unification (2)
- infinitary lambda calculus (2)
- lambda-calculus (2)
- lazy evaluation (2)
- logics in artificial intelligence (2)
- non-determinism (2)
- nondeterminism (2)
- programming languages (2)
- rewriting (2)
- second order unification (2)
- unification (2)
- Abstrakte Reduktion (1)
- Alice ML (1)
- Baumgrammatiken (1)
- Call-by-Need (1)
- Clean (1)
- Contextual Equivalence (1)
- Correctness (1)
- Futures (1)
- Haskell (1)
- Kontextuelle Gleicheit (1)
- Lambda Calculus (1)
- Letrec-Kalkül (1)
- ML <Programmiersprache> (1)
- Nichtdeterminismus (1)
- Operational Semantics (1)
- Polynomielles Wortproblem (1)
- Program Transformations (1)
- Programmkalküle (1)
- Programmkorrektheit (1)
- Sharing (1)
- Striktheitsanalyse (1)
- Termination (1)
- Wortproblem (1)
- abstract reduction (1)
- adequate translation (1)
- bisimulation (1)
- call-by-need evaluation (1)
- call-by-need lambda calculus (1)
- formal semantics (1)
- grammar-based compression (1)
- nominal unification (1)
- parallel processes (1)
- polynomial word problem (1)
- precongruence (1)
- program correctness (1)
- programming calculi (1)
- randomized algorithms (1)
- sharing (1)
- similarity (1)
- simulation (1)
- space improvements (1)
- space optimization (1)
- straight line programs (1)
- strictness analysis (1)
- translation (1)
- tree grammars (1)
- verzögerte Auswertung (1)
Institute
- Informatik (96)
We consider the problem of unifying a set of equations between second-order terms. Terms are constructed from function symbols, constant symbols and variables, and furthermore using monadic second-order variables that may stand for a term with one hole, and parametric terms. We consider stratified systems, where for every first-order and second-order variable, the string of second-order variables on the path from the root of a term to every occurrence of this variable is always the same. It is shown that unification of stratified second-order terms is decidable by describing a nondeterministic decision algorithm that eventually uses Makanin's algorithm for deciding the unifiability of word equations. As a generalization, we show that the method can be used as a unification procedure for non-stratified second-order systems, and describe conditions for termination in the general case.