Luca Roversi

Theor. Comput. Sci., 2025

2024

Certifying expressive power and algorithms of reversible primitive permutations with Lean.

[BibT_eX]

[DOI]

Giacomo Maletto

J. Log. Algebraic Methods Program., January, 2024

Quantum-Classical Sentiment Analysis.

[BibT_eX]

[DOI]

Mario Bifulco

CoRR, 2024

Algorithmically Expressive, Always-Terminating Model for Reversible Computation.

[BibT_eX]

[DOI]

Matteo Palazzo

Proceedings of the Reversible Computation - 16th International Conference, 2024

Host-Core Calculi for Non-classical Computations: A First Insight.

[BibT_eX]

[DOI]

Proceedings of the 25th Italian Conference on Theoretical Computer Science, 2024

2022

Programming the Interaction with Quantum Coprocessors.

[BibT_eX]

[DOI]

Ferruccio Damiani

ERCIM News, 2022

Certifying Algorithms and Relevant Properties of Reversible Primitive Permutations with Lean.

[BibT_eX]

[DOI]

Giacomo Maletto

Proceedings of the Reversible Computation - 14th International Conference, 2022

2021

Interleaving classical and reversible.

[BibT_eX]

[DOI]

CoRR, 2021

Splitting Recursion Schemes into Reversible and Classical Interacting Threads.

[BibT_eX]

[DOI]

Proceedings of the Reversible Computation - 13th International Conference, 2021

2020

A class of Recursive Permutations which is Primitive Recursive complete.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2020

The fixed point problem of a simple reversible language.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2020

A type-assignment of linear erasure and duplication.

[BibT_eX]

[DOI]

Gianluca Curzi

Theor. Comput. Sci., 2020

Probabilistic Soft Type Assignment.

[BibT_eX]

[DOI]

Gianluca Curzi

CoRR, 2020

On the Expressivity of Total Reversible Programming Languages.

[BibT_eX]

[DOI]

Proceedings of the Reversible Computation - 12th International Conference, 2020

2019

Introducing Yet Another REversible Language.

[BibT_eX]

[DOI]

Claudio Grandi

Dariush Moshiri

CoRR, 2019

2018

On a Class of Reversible Primitive Recursive Functions and Its Turing-Complete Extensions.

[BibT_eX]

[DOI]

New Gener. Comput., 2018

Subatomic systems need not be subatomic.

[BibT_eX]

[DOI]

CoRR, 2018

Quantum programming made easy.

[BibT_eX]

[DOI]

Margherita Zorzi

Proceedings of the Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, 2018

The Fixed Point Problem for General and for Linear SRL Programs is Undecidable.

[BibT_eX]

[DOI]

Proceedings of the 19th Italian Conference on Theoretical Computer Science, 2018

2016

A deep inference system with a self-dual binder which is complete for linear lambda calculus.

[BibT_eX]

[DOI]

J. Log. Comput., 2016

2015

Light combinators for finite fields arithmetic.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

A Class of Reversible Primitive Recursive Functions.

[BibT_eX]

[DOI]

Proceedings of the 16th Italian Conference on Theoretical Computer Science, 2015

A Certified Study of a Reversible Programming Language.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Types for Proofs and Programs, 2015

2013

Can a Light Typing Discipline Be Compatible with an Efficient Implementation of Finite Fields Inversion?

[BibT_eX]

[DOI]

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2013

2012

Intersection Types from a Proof-theoretic Perspective.

[BibT_eX]

[DOI]

Elaine Pimentel

Fundam. Informaticae, 2012

Communication, and concurrency with logic-based restriction inside a calculus of structures

[BibT_eX]

[DOI]

CoRR, 2012

Extending a system in the calculus of structures with a self-dual quantifier

[BibT_eX]

[DOI]

CoRR, 2012

2011

A Modular Database Architecture Enabled to Comparative Sequence Analysis.

[BibT_eX]

[DOI]

Trans. Large Scale Data Knowl. Centered Syst., 2011

Linear Lambda Calculus and Deep Inference.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, 2011

Typing a Core Binary-Field Arithmetic in a Light Logic.

[BibT_eX]

[DOI]

Emanuele Cesena

Marco Pedicini

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2011

2010

Linear lambda calculus with explicit substitutions as proof-search in Deep Inference

[BibT_eX]

[DOI]

CoRR, 2010

Safe Recursion on Notation into a Light Logic by Levels

[BibT_eX]

[DOI]

Proceedings of the Proceedings International Workshop on Developments in Implicit Computational complExity, 2010

2009

A By-Level Analysis of Multiplicative Exponential Linear Logic.

[BibT_eX]

[DOI]

Marco Gaboardi

Proceedings of the Mathematical Foundations of Computer Science 2009, 2009

Taming Modal Impredicativity: Superlazy Reduction.

[BibT_eX]

[DOI]

Ugo Dal Lago

Proceedings of the Logical Foundations of Computer Science, International Symposium, 2009

A Local Criterion for Polynomial-Time Stratified Computations.

[BibT_eX]

[DOI]

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2009

2008

Weak Affine Light Typing is complete with respect to Safe Recursion on Notation

[BibT_eX]

[DOI]

CoRR, 2008

Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Conference, 2008

2007

Weak Affine Light Typing: Polytime intensional expressivity, soundness and completeness

[BibT_eX]

[DOI]

CoRR, 2007

2003

Higher-Order Linear Ramified Recurrence.

[BibT_eX]

[DOI]

Ugo Dal Lago

Simone Martini

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

2002

Intuitionistic Light Affine Logic.

[BibT_eX]

[DOI]

Andrea Asperti

ACM Trans. Comput. Log., 2002

2001

Intersection Logic.

[BibT_eX]

[DOI]

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

2000

Light Affine Logic as a Programming Language: A First Contribution.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2000

Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)

[BibT_eX]

[DOI]

Andrea Asperti

CoRR, 2000

1999

The call-by-value [lambda]-calculus: a semantic investigation.

[BibT_eX]

[DOI]

Alberto Pravato

Math. Struct. Comput. Sci., 1999

A P-Time Completeness Proof for Light Logics.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 13th International Workshop, 1999

1998

A Polymorphic Language Which Is Typable and Poly-step.

[BibT_eX]

[DOI]

Proceedings of the Advances in Computing Science, 1998

1997

Lambda Calculus and Intuitionistic Linear Logic.

[BibT_eX]

[DOI]

Stud Logica, 1997

1996

A Type-Free Resource-Aware Lambda-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 10th International Workshop, 1996

1995

Categorical semantics of the call-by-value lambda-calculus.

[BibT_eX]

[DOI]

Alberto Pravato