Strong Call-by-Value is Reasonable, Implosively

Autor: Accattoli, Beniamino, Condoluci, Andrea, Coen, Claudio Sacerdoti

Whether the number of beta-steps in the lambda-calculus can be taken as a reasonable time cost model (that is, polynomially related to the one of Turing machines) is a delicate problem, which depends on the notion of evaluation strategy. Since the ni

Externí odkaz: http://arxiv.org/abs/2102.06928

Crumbling Abstract Machines

Autor: Accattoli, Beniamino, Condoluci, Andrea, Guerrieri, Giulio, Coen, Claudio Sacerdoti

Extending the lambda-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing sharing points in between any two of them, reducing to the case where

Externí odkaz: http://arxiv.org/abs/1907.06057

CERES in Propositional Proof Schemata

Autor: Condoluci, Andrea

Cut-elimination is one of the most famous problems in proof theory, and it was defined and solved for first-order sequent calculus by Gentzen in his celebrated Hauptsatz. Ceres is a different cut-elimination algorithm for first- and higher-order clas

Externí odkaz: http://arxiv.org/abs/1701.05251

Crumbling Abstract Machines

Autor: Claudio Sacerdoti Coen, Beniamino Accattoli, Giulio Guerrieri, Andrea Condoluci

Publikováno v: PPDP 2019-21st International Symposium on Principles and Practice of Programming Languages
PPDP 2019-21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. ⟨10.1145/3354166.3354169⟩
PPDP

International audience; Extending the λ-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing sharing points in between any two of them, reducin

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f2bcede1f56dba259666cec004ed1430
https://hal.archives-ouvertes.fr/hal-02415766/document

Admissible Tools in the Kitchen of Intuitionistic Logic

Autor: Matteo Manighetti, Andrea Condoluci

Publikováno v: Seventh International Workshop on Classical Logic and Computation (CL&C 2018)
Seventh International Workshop on Classical Logic and Computation (CL&C 2018), Jul 2018, Oxford, United Kingdom. pp.10-23
Electronic Proceedings in Theoretical Computer Science, Vol 281, Iss Proc. CL&C 2018, Pp 10-23 (2018)
CL&C

The usual reading of logical implication "A implies B" as "if A then B" fails in intuitionistic logic: there are formulas A and B such that "A implies B" is not provable, even though B is provable whenever A is provable. Intuitionistic rules apparent

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::33826f768c88f1a522c280f883533bc5
https://inria.hal.science/hal-01870112