Andrea Asperti

Salvatore Fiorilla

Lorenzo Orsini

Sensors, February, 2024

Wind speed super-resolution and validation: from ERA5 to CERRA via diffusion models.

[BibT_eX]

[DOI]

Fabio Merizzi

Stefano Colamonaco

CoRR, 2024

2023

Image embedding for denoising generative models.

[BibT_eX]

[DOI]

Artif. Intell. Rev., December, 2023

Deep Learning for Head Pose Estimation: A Survey.

[BibT_eX]

[DOI]

Daniele Filippini

SN Comput. Sci., July, 2023

Comparing the latent space of generative models.

[BibT_eX]

[DOI]

Valerio Tonelli

Neural Comput. Appl., February, 2023

Precipitation nowcasting with generative diffusion models.

[BibT_eX]

[DOI]

CoRR, 2023

Head Rotation in Denoising Diffusion Models.

[BibT_eX]

[DOI]

Gabriele Colasuonno

Antonio Guerra

CoRR, 2023

2022

Enhancing Variational Generation Through Self-Decomposition.

[BibT_eX]

[DOI]

Laura Bugo

Daniele Filippini

IEEE Access, 2022

MicroRacer: A Didactic Environment for Deep Reinforcement Learning.

[BibT_eX]

[DOI]

Marco Del Brutto

Proceedings of the Machine Learning, Optimization, and Data Science, 2022

2021

A Survey on Variational Autoencoders from a Green AI Perspective.

[BibT_eX]

[DOI]

Davide Evangelista

Elena Loli Piccolomini

SN Comput. Sci., 2021

Syllabification of the Divine Comedy.

[BibT_eX]

[DOI]

Stefano Dal Bianco

ACM Journal on Computing and Cultural Heritage, 2021

A survey on Variational Autoencoders from a GreenAI perspective.

[BibT_eX]

[DOI]

Davide Evangelista

Elena Loli Piccolomini

CoRR, 2021

Dissecting FLOPs Along Input Dimensions for GreenAI Cost Estimations.

[BibT_eX]

[DOI]

Davide Evangelista

Moreno Marzolla

Proceedings of the Machine Learning, Optimization, and Data Science, 2021

2020

Crawling in Rogue's Dungeons With Deep Reinforcement Techniques.

[BibT_eX]

[DOI]

IEEE Trans. Games, 2020

Balancing Reconstruction Error and Kullback-Leibler Divergence in Variational Autoencoders.

[BibT_eX]

[DOI]

Matteo Trentin

IEEE Access, 2020

Variance Loss in Variational Autoencoders.

[BibT_eX]

[DOI]

Proceedings of the Machine Learning, Optimization, and Data Science, 2020

2019

About Generative Aspects of Variational Autoencoders.

[BibT_eX]

[DOI]

Proceedings of the Machine Learning, Optimization, and Data Science, 2019

2018

Sparsity in Variational Autoencoders.

[BibT_eX]

[DOI]

CoRR, 2018

Crawling in Rogue's Dungeons with (Partitioned) A3C.

[BibT_eX]

[DOI]

Daniele Cortesi

Francesco Sovrano

Proceedings of the Machine Learning, Optimization, and Data Science, 2018

The Effectiveness of Data Augmentation for Detection of Gastrointestinal Diseases from Endoscopical Images.

[BibT_eX]

[DOI]

Claudio Mastronardo

Proceedings of the 11th International Joint Conference on Biomedical Engineering Systems and Technologies (BIOSTEC 2018), 2018

2017

About the efficient reduction of lambda terms.

[BibT_eX]

[DOI]

CoRR, 2017

Automatic verification and interactive theorem proving.

[BibT_eX]

[DOI]

CoRR, 2017

2015

Computational Complexity Via Finite Types.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2015

A formalization of multi-tape Turing machines.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2015

Reverse Complexity.

[BibT_eX]

[DOI]

J. Autom. Reason., 2015

The Speedup Theorem in a Primitive Recursive Framework.

[BibT_eX]

[DOI]

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

Matita Tutorial.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2014

2013

The Cost of Usage in the Lambda-Calculus.

[BibT_eX]

[DOI]

Jean-Jacques Lévy

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

A Machine-Checked Proof of the Odd Order Theorem.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

A proof of Bertrand's postulate.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2012

Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Formalizing Turing Machines.

[BibT_eX]

[DOI]

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

Type systems for dummies.

[BibT_eX]

[DOI]

Ferruccio Guidi

Proceedings of the 8th ACM SIGPLAN Workshop on Types in Languages Design and Implementation, 2012

A Compact Proof of Decidability for Regular Expression Equivalence.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Rating Disambiguation Errors.

[BibT_eX]

[DOI]

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

A Web Interface for Matita.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

Proof, Message and Certificate.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011

Certified Complexity.

[BibT_eX]

[DOI]

Ian Stark

Proceedings of the 2nd European Future Technologies Conference and Exhibition, 2011

Zen and the art of formalisation.

[BibT_eX]

[DOI]

Jeremy Avigad

Math. Struct. Comput. Sci., 2011

Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.

[BibT_eX]

[DOI]

Maria Emilia Maietti

Giovanni Sambin

Silvio Valentini

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

The Matita Interactive Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Regular Expressions, au point

[BibT_eX]

[DOI]

CoRR, 2010

Smart Matching.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

Some Considerations on the Usability of Interactive Provers.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009

Social processes, program verification and all that.

[BibT_eX]

[DOI]

Herman Geuvers

Raja Natarajan

Math. Struct. Comput. Sci., 2009

Mobile Petri nets.

[BibT_eX]

[DOI]

Nadia Busi

Math. Struct. Comput. Sci., 2009

Preface.

[BibT_eX]

[DOI]

Roberto M. Amadio

Giuseppe Castagna

Inf. Comput., 2009

Superposition as a logical glue

[BibT_eX]

[DOI]

Proceedings of the Proceedings Types for Proofs and Programs, Revised Selected Papers, 2009

Hints in Unification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

2008

A Page in Number Theory.

[BibT_eX]

[DOI]

Cristian Armentano

J. Formaliz. Reason., 2008

An Interactive Driver for Goal-directed Proof Strategies.

[BibT_eX]

[DOI]

Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, 2008

About the Formalization of Some Results by Chebyshev in Number Theory.

[BibT_eX]

[DOI]

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

The intensional content of Rice's theorem.

[BibT_eX]

[DOI]

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

2007

User Interaction with the Matita Proof Assistant.

[BibT_eX]

[DOI]

Stefano Zacchiroli

J. Autom. Reason., 2007

Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case.

[BibT_eX]

[DOI]

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2006

Crafting a Proof Assistant.

[BibT_eX]

[DOI]

Stefano Zacchiroli

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

2005

An Interactive Algebra Course with Formalised Proofs and Definitions.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

2004

(Optimal) duplication is not elementary recursive.

[BibT_eX]

[DOI]

Paolo Coppola

Simone Martini

Inf. Comput., 2004

A Content Based Mathematical Search Engine: Whelp.

[BibT_eX]

[DOI]

Ferruccio Guidi

Stefano Zacchiroli

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

Efficient Retrieval of Mathematical Statements.

[BibT_eX]

[DOI]

Matteo Selmi

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

2003

Mathematical Knowledge Management in HELM.

[BibT_eX]

[DOI]

Luca Padovani

Ferruccio Guidi

Irene Schena

Ann. Math. Artif. Intell., 2003

2002

Intuitionistic Light Affine Logic.

[BibT_eX]

[DOI]

Luca Roversi

ACM Trans. Comput. Log., 2002

MOWGLI - An Approach to Machine-Understandable Representation of the Mathematical Information in Digital Documents.

[BibT_eX]

[DOI]

Bernd Wegner

Proceedings of the Electronic Information and Communication in Mathematics, 2002

2001

Parallel Beta Reduction Is Not Elementary Recursive.

[BibT_eX]

[DOI]

Harry G. Mairson

Inf. Comput., 2001

HELM and the Semantic Math-Web.

[BibT_eX]

[DOI]

Luca Padovani

Irene Schena

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

XML, Stylesheets and the Re-mathematization of Formal Content.

[BibT_eX]

[DOI]

Luca Padovani

Irene Schena

Proceedings of the Extreme Markup Languages® 2001 Conference, 2001

2000

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

[BibT_eX]

[DOI]

Luca Roversi

CoRR, 2000

1998

Optimal Reduction of Functional Expressions.

[BibT_eX]

[DOI]

Proceedings of the Principles of Declarative Programming, 10th International Symposium, 1998

Light Affine Logic.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

The optimal implementation of functional programming languages.

[BibT_eX]

Stefano Guerrini

Cambridge tracts in theoretical computer science 45, Cambridge University Press, ISBN: 978-0-521-62112-0, 1998

1997

A Sufficient Condition for Completability of Partial Combinatory Algebras.

[BibT_eX]

[DOI]

Agata Ciabattoni

J. Symb. Log., 1997

Safe Operators: Brackets Closed Forever Optimizing Optimal lambda-Calculus Implementations - Optimizing Optimal lambda-Calculus Implementations.

[BibT_eX]

[DOI]

Juliusz Chroboczek

Appl. Algebra Eng. Commun. Comput., 1997

On the Dynamics of Sharing Graphs.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 24th International Colloquium, 1997

1996

Interaction Systems II: The Practice of Optimal Reductions.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1996

The Bologna Optimal Higher-Order Machine.

[BibT_eX]

[DOI]

Cecilia Giovanetti

Andrea Naletto

J. Funct. Program., 1996

On the Complexity of Beta-Reduction.

[BibT_eX]

[DOI]

Proceedings of the Conference Record of POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1996

1995

Paths, Computations and Labels in the lambda-Calculus.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1995

Causal Dependencies in Multiplicative Linear Logic with MIX.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1995

Linear Logic, Comonads and Optimal Reduction.

[BibT_eX]

[DOI]

Fundam. Informaticae, 1995

Comparing Lambda-calculus translations in Sharing Graphs.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1995

deltao!Epsilon = 1 - Optimizing Optimal lambda-Calculus Implementations.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

Effective Applicative Structures.

[BibT_eX]

[DOI]

Agata Ciabattoni

Proceedings of the Category Theory and Computer Science, 6th International Conference, 1995

1994

Interaction Systems I: The Theory of Optimal Reductions.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1994

The Family Relation in Interaction Systems.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computer Software, 1994

Paths in the lambda-calculus

[BibT_eX]

[DOI]

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Yet Another Correctness Criterion for Multiplicative Linear Logic with MIX.

[BibT_eX]

[DOI]

Giovanna M. Dore

Proceedings of the Logical Foundations of Computer Science, Third International Symposium, 1994

Category Theory: Basic notions and general philosophy.

[BibT_eX]

Proceedings of the JFPLC'94, 1994

1993

Optimal Reductions in Interaction Systems.

[BibT_eX]

[DOI]

Proceedings of the TAPSOFT'93: Theory and Practice of Software Development, 1993

Interaction Systems.

[BibT_eX]

[DOI]

Proceedings of the Higher-Order Algebra, 1993

1992

Categorical Models of Polymorphism

[BibT_eX]

[DOI]

Simone Martini

Inf. Comput., July, 1992

A Categorical Understanding of Environment Machines.

[BibT_eX]

[DOI]

J. Funct. Program., 1992

A Categorial Model for Logic Programs: Indexed Monoidal Categories.

[BibT_eX]

[DOI]

Andrea Corradini

Proceedings of the Sematics: Foundations and Applications, 1992

1991

Categories, types and structures - an introduction to category theory for the working computer scientist.

[BibT_eX]

Giuseppe Longo

Foundations of computing, MIT Press, ISBN: 978-0-262-01125-9, 1991

1990

Stability and Computability in Coherent Domains

[BibT_eX]

[DOI]

Inf. Comput., June, 1990

Implicative Formulae in the "Proofs as Computations" Analogy.

[BibT_eX]

[DOI]

Gian-Luigi Ferrari

Roberto Gorrieri

Proceedings of the Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, 1990

Integrating Strict and Lazy Evaluation: The lambda-sl-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Programming Language Implementation and Logic Programming, 1990

1989

Projections Instead of Variables: A Category Theoretic Interpretation of Logic Programs.

[BibT_eX]

Simone Martini

Proceedings of the Logic Programming, 1989

1986

Relating Type-Structures: Partial Variations on a Theme of Friedman and Statman.

[BibT_eX]

[DOI]