Alejandro Ríos

Andrés Viso

CoRR, 2020

Pure Pattern Calculus à la de Bruijn.

[BibT_eX]

[DOI]

Alexis Martin

Andrés Viso

Proceedings of the 15th International Workshop on Logical and Semantic Frameworks with Applications, 2020

2019

Projections for infinitary rewriting (extended version).

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2019

2018

Call-by-Need, Neededness and All That.

[BibT_eX]

[DOI]

Andrés Viso

Proceedings of the Foundations of Software Science and Computation Structures, 2018

2017

On abstract normalisation beyond neededness.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2017

2016

Projections for Infinitary Rewriting.

[BibT_eX]

[DOI]

Proceedings of the 11th Workshop on Logical and Semantic Frameworks with Applications, 2016

2014

Proof terms for infinitary rewriting, progress report.

[BibT_eX]

[DOI]

CoRR, 2014

An abstract normalisation result with applications to non-sequential calculi.

[BibT_eX]

[DOI]

CoRR, 2014

Proof Terms for Infinitary Rewriting.

[BibT_eX]

[DOI]

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

2012

Normalisation for Dynamic Pattern Calculi.

[BibT_eX]

[DOI]

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

2010

A standardisation proof for algebraic pattern calculi

[BibT_eX]

[DOI]

Proceedings of the Proceedings 5th International Workshop on Higher-Order Rewriting, 2010

Swapping: a natural bridge between named and indexed explicit substitution calculi

[BibT_eX]

[DOI]

Ariel Mendelzon

Beta Ziliani

Proceedings of the Proceedings 5th International Workshop on Higher-Order Rewriting, 2010

2009

The lambda-calculus with constructors: Syntax, confluence and separation.

[BibT_eX]

[DOI]

Ariel Arbiser

Alexandre Miquel

J. Funct. Program., 2009

2007

The Weak Normalization of the Simply Typed lambda-se-calculus.

[BibT_eX]

[DOI]

Ariel Arbiser

Log. J. IGPL, 2007

2006

A Lambda-Calculus with Constructors.

[BibT_eX]

[DOI]

Ariel Arbiser

Alexandre Miquel

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

2005

Relating Higher-order and First-order Rewriting.

[BibT_eX]

[DOI]

J. Log. Comput., 2005

de Bruijn Indices for Metaterms.

[BibT_eX]

[DOI]

J. Log. Comput., 2005

2003

Explicit substitutions à la de Bruijn: the local and global way.

[BibT_eX]

[DOI]

Proceedings of the Mathematics, 2003

2002

Pure Type Systems with de Bruijn Indices.

[BibT_eX]

[DOI]

Comput. J., 2002

2001

From Higher-Order to First-Order Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001

2000

Relating the λσ- and λs-styles of explicit substitutions.

[BibT_eX]

[DOI]

J. Log. Comput., 2000

A de Bruijn Notation for Higher-Order Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 11th International Conference, 2000

1998

Calculi of Generalized beta-Reduction and Explicit Substitutions: The Type-Free and Simply Typed Versions.

[BibT_eX]

[DOI]

J. B. Wells

J. Funct. Log. Program., 1998

Bridging de Bruijn Indices and Variable Names in Explicit Substitutions Calculi.

[BibT_eX]

[DOI]

Log. J. IGPL, 1998

1997

Extending a lambda-Calculus with Explicit Substitution which Preserves Strong Normalisation Into a Confluent Calculus on Open Terms.

[BibT_eX]

[DOI]

J. Funct. Program., 1997

Explicit Substitutions for the Lambda-Calculus.

[BibT_eX]

[DOI]

Gilles Barthe

Proceedings of the Algebraic and Logic Programming, 6th International Joint Conference, 1997

1996

Strong Normalizations of Substitutions.

[BibT_eX]

[DOI]

Pierre-Louis Curien

Thérèse Hardin

J. Log. Comput., 1996

Generalized beta-Reduction and Explicit Substitution.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages: Implementations, 1996

1995

A Lambda-Calculus à la de Bruijn with Explicit Substitutions

[BibT_eX]

[DOI]

Proceedings of the Programming Languages: Implementations, 1995

1992

Strong Normalization of Substitutions.

[BibT_eX]

[DOI]

Pierre-Louis Curien

Thérèse Hardin