Delia Kesner

Log. Methods Comput. Sci., 2024

Genericity Through Stratification.

[BibT_eX]

[DOI]

Victor Arrial

Giulio Guerrieri

CoRR, 2024

The Ackermann Award 2023.

[BibT_eX]

[DOI]

Maribel Fernández

Jean Goubault-Larrecq

Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

2023

The bang calculus revisited.

[BibT_eX]

[DOI]

Inf. Comput., August, 2023

Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework.

[BibT_eX]

[DOI]

Victor Arrial

Giulio Guerrieri

Proc. ACM Program. Lang., January, 2023

Milner's Lambda-Calculus with Partial Substitutions.

[BibT_eX]

[DOI]

Shane Ó Conchúir

CoRR, 2023

Quantitative Global Memory.

[BibT_eX]

[DOI]

Sandra Alves

Miguel Ramos

Proceedings of the Logic, Language, Information, and Computation, 2023

2022

A fine-grained computational interpretation of Girard's intuitionistic proof-nets.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications (Long Version).

[BibT_eX]

[DOI]

José Espírito Santo

CoRR, 2022

Solvability for Generalized Applications.

[BibT_eX]

[DOI]

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

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications.

[BibT_eX]

[DOI]

José Espírito Santo

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

Encoding Tight Typing in a Unified Framework.

[BibT_eX]

[DOI]

Proceedings of the 30th EACSL Annual Conference on Computer Science Logic, 2022

2021

Solvability = Typability + Inhabitation.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2021

The Power of Tightness for Call-By-Push-Value.

[BibT_eX]

[DOI]

CoRR, 2021

A Strong Bisimulation for Control Operators by Means of Multiplicative and Exponential Reduction.

[BibT_eX]

[DOI]

CoRR, 2021

The Spirit of Node Replication.

[BibT_eX]

[DOI]

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

2020

Non-idempotent types for classical calculi in natural deduction style.

[BibT_eX]

[DOI]

Pierre Vial

Log. Methods Comput. Sci., 2020

Tight typings and split bounds, fully developed.

[BibT_eX]

[DOI]

Stéphane Graham-Lengrand

J. Funct. Program., 2020

Consuming and Persistent Types for Classical Logic.

[BibT_eX]

[DOI]

Pierre Vial

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Strong Bisimulation for Control Operators (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the 28th EACSL Annual Conference on Computer Science Logic, 2020

2019

A resource aware semantics for a focused intuitionistic calculus.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2019

Strong Bisimulation for Control Operators.

[BibT_eX]

[DOI]

CoRR, 2019

A Quantitative Understanding of Pattern Matching.

[BibT_eX]

[DOI]

Sandra Alves

Proceedings of the 25th International Conference on Types for Proofs and Programs, 2019

2018

Tight typings and split bounds.

[BibT_eX]

[DOI]

Stéphane Graham-Lengrand

Proc. ACM Program. Lang., 2018

Inhabitation for Non-idempotent Intersection Types.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2018

Observability = Typability + Inhabitation.

[BibT_eX]

[DOI]

CoRR, 2018

Call-by-Need, Neededness and All That.

[BibT_eX]

[DOI]

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

2017

On abstract normalisation beyond neededness.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2017

Foundations of strong call by need.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2017

Non-idempotent intersection types for the Lambda-Calculus.

[BibT_eX]

[DOI]

Log. J. IGPL, 2017

Types as Resources for Classical Natural Deduction.

[BibT_eX]

[DOI]

Pierre Vial

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

2016

Reasoning About Call-by-need by Means of Types.

[BibT_eX]

[DOI]

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

2015

Special Issue: Selected papers of the 7th and 8th workshops on Logical and Semantic Frameworks with Applications (LSFA).

[BibT_eX]

[DOI]

Marcelo Finger

Theor. Comput. Sci., 2015

Strong Normalization through Intersection Types and Memory.

[BibT_eX]

[DOI]

Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

Observability for Pair Pattern Calculi.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

A Resource Aware Computational Interpretation for Herbelin's Syntax.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2015, 2015

2014

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

[BibT_eX]

[DOI]

CoRR, 2014

A nonstandard standardization theorem.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Quantitative Types for the Linear Substitution Calculus.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 2014

The Inhabitation Problem for Non-idempotent Intersection Types.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 2014

Metaconfluence of Calculi with Explicit Substitutions at a Distance.

[BibT_eX]

[DOI]

Flávio L. C. de Moura

Mauricio Ayala-Rincón

Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014

2012

Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Normalisation for Dynamic Pattern Calculi.

[BibT_eX]

[DOI]

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

The Permutative λ-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

2011

A prismoid framework for languages with resources.

[BibT_eX]

[DOI]

Fabien Renaud

Theor. Comput. Sci., 2011

2010

A standardisation proof for algebraic pattern calculi

[BibT_eX]

[DOI]

Carlos Lombardi

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

The Structural <i>lambda</i>-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

First-class patterns.

[BibT_eX]

[DOI]

C. Barry Jay

J. Funct. Program., 2009

A Theory of Explicit Substitutions with Safe and Full Composition

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2009

The Prismoid of Resources.

[BibT_eX]

[DOI]

Fabien Renaud

Proceedings of the Mathematical Foundations of Computer Science 2009, 2009

2008

Perpetuality for Full and Safe Composition (in a Constructive Setting).

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

2007

Expression Reduction Systems with Patterns.

[BibT_eX]

[DOI]

Julien Forest

J. Autom. Reason., 2007

Resource operators for lambda-calculus.

[BibT_eX]

[DOI]

Stéphane Lengrand

Inf. Comput., 2007

The Theory of Calculi with Explicit Substitutions Revisited.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

2006

Pure Pattern Calculus.

[BibT_eX]

[DOI]

C. Barry Jay

Proceedings of the Programming Languages and Systems, 2006

Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic.

[BibT_eX]

[DOI]

Roy Dyckhoff

Stéphane Lengrand

Proceedings of the Automated Reasoning, Third International Joint 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

Extending the Explicit Substitution Paradigm.

[BibT_eX]

[DOI]

Stéphane Lengrand

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Expression Reduction Systems and Extensions: An Overview.

[BibT_eX]

[DOI]

John R. W. Glauert

Zurab Khasidashvili

Proceedings of the Processes, 2005

2004

Pattern matching as cut elimination.

[BibT_eX]

[DOI]

Serenella Cerrito

Theor. Comput. Sci., 2004

2003

Proof Nets And Explicit Substitutions.

[BibT_eX]

[DOI]

Emmanuel Polonowski

Math. Struct. Comput. Sci., 2003

2001

Theory and applications of explicit substitutions: Introduction.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2001

From Higher-Order to First-Order Rewriting.

[BibT_eX]

[DOI]

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

2000

Confluence of extensional and non-extensional lambda-calculi with explicit substitutions.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2000

A de Bruijn Notation for Higher-Order Rewriting.

[BibT_eX]

[DOI]

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

1999

Explicit Substitutions for Objects and Functions

[BibT_eX]

Pablo E. Martínez López

J. Funct. Log. Program., 1999

lambda-Calculi with Explicit Substitutions Preserving Strong Normalization.

[BibT_eX]

[DOI]

Maria C. F. Ferreira

Appl. Algebra Eng. Commun. Comput., 1999

1998

Reducing AC-Termination to Termination.

[BibT_eX]

[DOI]

Maria C. F. Ferreira

Proceedings of the Mathematical Foundations of Computer Science 1998, 1998

1997

Reasoning about Redundant Patterns.

[BibT_eX]

[DOI]

J. Funct. Log. Program., 1997

Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

1996

Combining Algebraic Rewriting, Extensional Lambda Calculi, and Fixpoints.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1996

A Typed Pattern Calculus.

[BibT_eX]

[DOI]

Val Tannen

Inf. Comput., 1996

Confluence Properties of Extensional and Non-Extensional <i>lambda</i>-Calculi with Explicit Substitutions (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

Lambda-Calculi with Explicit Substitutions and Composition Which Preserve Beta-Strong Normalization.

[BibT_eX]

[DOI]

Maria C. F. Ferreira

Proceedings of the Algebraic and Logic Programming, 5th International Conference, 1996

1995

Rewriting with Extensional Polymorphic Lambda-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 9th International Workshop, 1995

1994

Simulating Expansions without Expansions.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1994

Combining First Order Algebraic Rewriting Systems, Recursion and Extensional Lambda Calculi.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 21st International Colloquium, 1994

Reasoning about Layered, Wildcard and Product Patterns.

[BibT_eX]

[DOI]

Proceedings of the Algebraic and Logic Programming, 4th International Conference, 1994

1993

A Confluent Reduction for the Extensional Typed lambda-Calculus with Pairs, Sums, Recursion and terminal Object.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 20nd International Colloquium, 1993

1992

Free Sequentially in Orthogonal Order-Sorted Rewriting Systems with Constructors.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

1991

Pattern Matching in Order-Sorted Languages.

[BibT_eX]

[DOI]