Manfred Schmidt-Schauß

Daniele Nantes-Sobrinho

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2021

Minimal Translations from Synchronous Communication to Synchronizing Locks.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Combined 28th International Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics, 2021

Minimal Translations from Synchronous Communication to Synchronizing Locks (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2021

2020

Rewriting with generalized nominal unification.

[BibT_eX]

[DOI]

Yunus D. K. Kutz

Math. Struct. Comput. Sci., 2020

Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, 2020

Nominal Algorithms: Applications and Extensions.

[BibT_eX]

[DOI]

Proceedings of the 34th International Workshop on Unification, 2020

Nominal Unification with Letrec and Environment-Variables.

[BibT_eX]

[DOI]

Yunus D. K. Kutz

Proceedings of the Logic-Based Program Synthesis and Transformation, 2020

2019

Nominal unification with atom-variables.

[BibT_eX]

[DOI]

Yunus D. K. Kutz

J. Symb. Comput., 2019

A Note on Unification, Subsumption and Unification Type.

[BibT_eX]

[DOI]

Proceedings of the Description Logic, Theory Combination, and All That, 2019

2018

Linear pattern matching of compressed terms and polynomial rewriting.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2018

Optimizing Space of Parallel Processes.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, 2018

Nominal Unification with Atom and Context Variables.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

Sequential and Parallel Improvements in a Concurrent Functional Programming Language.

[BibT_eX]

[DOI]

Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, 2018

2017

Improvements in a call-by-need functional core language: Common subexpression elimination and resource preserving translations.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2017

Processing Succinct Matrices and Vectors.

[BibT_eX]

[DOI]

Markus Lohrey

Theory Comput. Syst., 2017

Space Improvements and Equivalences in a Functional Core Language.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation, 2017

2016

An Environment for Analyzing Space Optimizations in Call-by-Need Functional Languages.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation, 2016

A Call-by-Need Lambda Calculus with Scoped Work Decorations.

[BibT_eX]

[DOI]

Proceedings of the Gemeinsamer Tagungsband der Workshops der Tagung Software Engineering 2016 (SE 2016), 2016

Unification of program expressions with recursive bindings.

[BibT_eX]

[DOI]

Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, 2016

Nominal Unification of Higher Order Expressions with Recursive Let.

[BibT_eX]

[DOI]

Temur Kutsia

Proceedings of the Logic-Based Program Synthesis and Transformation, 2016

2015

Observational program calculi and the correctness of translations.

[BibT_eX]

[DOI]

Joachim Niehren

Jan Schwinghammer

Theor. Comput. Sci., 2015

Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2015

Observing Success in the Pi-Calculus.

[BibT_eX]

[DOI]

Proceedings of the 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, 2015

Improvements in a functional core language with call-by-need operational semantics.

[BibT_eX]

[DOI]

Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, 2015

One Context Unification Problems Solvable in Polynomial Time.

[BibT_eX]

[DOI]

Ashish Tiwari

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Sharing-aware improvements in a call-by-need functional core language.

[BibT_eX]

[DOI]

Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, 2015

Two-Restricted One Context Unification is in Polynomial Time.

[BibT_eX]

[DOI]

Ashish Tiwari

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report).

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation, 2014

Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB.

[BibT_eX]

[DOI]

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Concurrent Programming Languages and Methods for Semantic Analyses (Extended Abstract of Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

2013

A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial Functions.

[BibT_eX]

[DOI]

J. Autom. Reason., 2013

Linear Compressed Pattern Matching for Polynomial Rewriting (Extended Abstract)

[BibT_eX]

[DOI]

Proceedings of the Proceedings 7th International Workshop on Computing with Terms and Graphs, 2013

Algorithms for Extended Alpha-Equivalence and Complexity.

[BibT_eX]

[DOI]

Proceedings of the 24th International Conference on Rewriting Techniques and Applications, 2013

Extending Abramsky's Lazy Lambda Calculus: (Non)-Conservativity of Embeddings.

[BibT_eX]

[DOI]

Proceedings of the 24th International Conference on Rewriting Techniques and Applications, 2013

Correctness of an STM Haskell implementation.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

2012

Parameter reduction and automata evaluation for grammar-compressed trees.

[BibT_eX]

[DOI]

Markus Lohrey

Sebastian Maneth

J. Comput. Syst. Sci., 2012

Fast equality test for straight-line compressed strings.

[BibT_eX]

[DOI]

Georg Schnitger

Inf. Process. Lett., 2012

Matching of Compressed Patterns with Character-Variables.

[BibT_eX]

[DOI]

Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , 2012

Conservative Concurrency in Haskell.

[BibT_eX]

[DOI]

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Correctness of Program Transformations as a Termination Problem.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

Unification and matching on compressed terms.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2011

Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2011

On the complexity of Bounded Second-Order Unification and Stratified Context Unification.

[BibT_eX]

[DOI]

Log. J. IGPL, 2011

A Unification Algorithm to Compute Overlaps in a Call-by-Need Lambda-Calculus with Variable-Binding Chains.

[BibT_eX]

[DOI]

Proceedings of the 25th International Workshop on Unification, 2011

Frontmatter, Table of Contents, Preface, Conference Organization.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

A contextual semantics for concurrent Haskell with futures.

[BibT_eX]

[DOI]

Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Congruence Closure of Compressed Terms in Polynomial Time.

[BibT_eX]

[DOI]

Altug Anis

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

2010

On generic context lemmas for higher-order calculi with sharing.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2010

Context unification with one context variable.

[BibT_eX]

[DOI]

Ashish Tiwari

J. Symb. Comput., 2010

Closures of may-, should- and must-convergences for contextual equivalence.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2010

Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi.

[BibT_eX]

[DOI]

Matthias Mann

Inf. Comput., 2010

Towards Correctness of Program Transformations Through Unification and Critical Pair Computation

[BibT_eX]

[DOI]

Proceedings of the Proceedings 24th International Workshop on Unification, 2010

Simulation in the Call-by-Need Lambda-Calculus with letrec.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Rewriting Techniques and Applications, 2010

2009

Unification with Singleton Tree Grammars.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 20th International Conference, 2009

Reasoning about Contextual Equivalence: From Untyped to Polymorphically Typed Calculi.

[BibT_eX]

[DOI]

Frederik Harwath

Proceedings of the 39. Jahrestagung der Gesellschaft für Informatik, Im Focus das Leben, INFORMATIK 2009, Lübeck, Germany, September 28, 2009

Parameter Reduction in Grammar-Compressed Trees.

[BibT_eX]

[DOI]

Markus Lohrey

Sebastian Maneth

Proceedings of the Foundations of Software Science and Computational Structures, 2009

2008

The Complexity of Monadic Second-Order Unification.

[BibT_eX]

[DOI]

SIAM J. Comput., 2008

A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2008

Safety of Nöcker's strictness analysis.

[BibT_eX]

[DOI]

Marko Schütz

J. Funct. Program., 2008

A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 19th International Conference, 2008

Context Matching for Compressed Terms.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

Adequacy of Compositional Translations for Observational Semantics.

[BibT_eX]

[DOI]

Joachim Niehren

Jan Schwinghammer

Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

2007

Deciding inclusion of set constants over infinite non-strict data structures.

[BibT_eX]

[DOI]

Marko Schütz

RAIRO Theor. Informatics Appl., 2007

Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures.

[BibT_eX]

[DOI]

Joachim Niehren

Jan Schwinghammer

Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, 2007

Correctness of Copy in Calculi with Letrec.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

2006

Bounded Second-Order Unification Is NP-Complete.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Stratified Context Unification Is NP-Complete.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Decidability of bounded higher-order unification.

[BibT_eX]

[DOI]

Klaus U. Schulz

J. Symb. Comput., 2005

Decidable Variants of Higher-Order Unification.

[BibT_eX]

[DOI]

Proceedings of the Mechanizing Mathematical Reasoning, 2005

2004

The Complexity of Linear and Stratified Context Matching Problems.

[BibT_eX]

[DOI]

Jürgen Stuber

Theory Comput. Syst., 2004

Decidability of bounded second order unification.

[BibT_eX]

[DOI]

Inf. Comput., 2004

Monadic Second-Order Unification Is NP-Complete.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 15th International Conference, 2004

2003

Decidability of Arity-Bounded Higher-Order Matching.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

A Decision Algorithm for Stratified Context Unification.

[BibT_eX]

[DOI]

J. Log. Comput., 2002

Solvability of Context Equations with Two Context Variables is Decidable.

[BibT_eX]

[DOI]

Klaus U. Schulz

J. Symb. Comput., 2002

2001

A Term-Based Approach to Project Scheduling.

[BibT_eX]

[DOI]

Pok-Son Kim

Proceedings of the Conceptual Structures: Broadening the Base, 2001

Stratified Context Unification Is in PSPACE.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 15th International Workshop, 2001

2000

A Lambda-Calculus with letrec, case, constructors and non-determinism

[BibT_eX]

[DOI]

Michael Huber

CoRR, 2000

1999

Decidability of Behavioural Equivalence in Unary PCF.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1999

1998

A Decision Algorithm for Distributive Unification.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1998

On the Exponent of Periodicity of Minimal Solutions of Context Equation.

[BibT_eX]

[DOI]

Klaus U. Schulz

Proceedings of the Rewriting Techniques and Applications, 9th International Conference, 1998

A Non-Deterministic Call-by-Need Lambda Calculus.

[BibT_eX]

[DOI]

Arne Kutzner

Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), 1998

1997

Natural Expert: A Commercial Functional Programming Environment.

[BibT_eX]

[DOI]

Nigel W. O. Hutchison

Ute Neuhaus

Cordelia V. Hall

J. Funct. Program., 1997

TEA: Automatically Proving Termination of Programs in a Non-strict Higher-Order Functional Language.

[BibT_eX]

[DOI]

Sven Eric Panitz

Proceedings of the Static Analysis, 4th International Symposium, 1997

1996

Decidability of Unification in the Theory of One-Sided Distributivity and a Multiplicative Unit.

[BibT_eX]

[DOI]

J. Symb. Comput., 1996

1995

Modular Termination of r-Consistent and Left-Linear Term Rewriting Systems.

[BibT_eX]

[DOI]

Massimo Marchiori

Sven Eric Panitz

Theor. Comput. Sci., 1995

An Algorithm for Distributive Unification.

[BibT_eX]

Proceedings of the 9th International Workshop on Unification, 1995

Abstract Reduction Using a Tableau Calculus

[BibT_eX]

[DOI]

Sven Eric Panitz

Marko Schütz

Proceedings of the Static Analysis, 1995

1993

Unification Under One-Sided Distributivity with a Multiplicative Unit.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming and Automated Reasoning,4th International Conference, 1993

1991

Attributive Concept Descriptions with Complements.

[BibT_eX]

[DOI]

Gert Smolka

Artif. Intell., 1991

External Function Calls in a Functional Language.

[BibT_eX]

[DOI]

Proceedings of the Functional Programming, 1991

1990

Subsumption Algorithms for Concept Description Languages.

[BibT_eX]

Bernhard Hollunder

Werner Nutt

Proceedings of the 9th European Conference on Artificial Intelligence, 1990

1989

Attributive Concept Descriptions with Unions and Complements

[BibT_eX]

Gert Smolka

IWBS Report, 1989

Unification in Permutative Equational Theories is Undecidable.

[BibT_eX]

[DOI]

J. Symb. Comput., 1989

Unification in a Combination of Arbitrary Disjoint Equational Theories.

[BibT_eX]

[DOI]

J. Symb. Comput., 1989

On Equational Theories, Unification, and (Un)Decidability.

[BibT_eX]

[DOI]

Hans-Jürgen Bürckert

Alexander Herold

J. Symb. Comput., 1989

Unification in Boolean Rings and Abelian Groups.

[BibT_eX]

[DOI]

Alexandre Boudet

Jean-Pierre Jouannaud

J. Symb. Comput., 1989

Subsumption in KL-ONE is Undecidable.

[BibT_eX]

Proceedings of the 1st International Conference on Principles of Knowledge Representation and Reasoning (KR'89). Toronto, 1989

Computational Aspects of an Order-Sorted Logic with Term Declarations

[BibT_eX]

[DOI]

Lecture Notes in Computer Science 395, Springer, ISBN: 3-540-51705-7, 1989

1988

Implication of Clauses is Undecidable.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1988

Bericht zur 9th Conference on Automated Deduction.

[BibT_eX]

Hans Jürgen Ohlbach

Künstliche Intell., 1988

Unification in Free Extensions of Boolean Rings and Abelian Groups

[BibT_eX]

[DOI]

Alexandre Boudet

Jean-Pierre Jouannaud

Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

Computational aspects of an order-sorted logic with term declarations.

[BibT_eX]

[DOI]

PhD thesis, 1988

1987

On Equational Theories, Unification and Decidability.

[BibT_eX]

[DOI]

Hans-Jürgen Bürckert

Alexander Herold

Proceedings of the Rewriting Techniques and Applications, 2nd International Conference, 1987

1986

Unification under Associativity and Idempotence is of Type Nullary.

[BibT_eX]

[DOI]

J. Autom. Reason., 1986

Unification in Many-Sorted Eqational Theories.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985

The Lion and the Unicorn.

[BibT_eX]

[DOI]

Hans Jürgen Ohlbach

J. Autom. Reason., 1985

Unification in a Many-sorted Calculus with Declarations.

[BibT_eX]

[DOI]

Proceedings of the GWAI-85, 1985

A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation.

[BibT_eX]