Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Stefano Berardi
@inproceedings{DBLP:conf/csl/BerardiB024,
author = {Stefano Berardi and
Gabriele Buriola and
Peter Schuster},
editor = {Aniello Murano and
Alexandra Silva},
title = {A General Constructive Form of Higman's Lemma},
booktitle = {32nd {EACSL} Annual Conference on Computer Science Logic, {CSL} 2024,
February 19-23, 2024, Naples, Italy},
series = {LIPIcs},
volume = {288},
pages = {16:1--16:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2024},
url = {https://doi.org/10.4230/LIPIcs.CSL.2024.16},
doi = {10.4230/LIPICS.CSL.2024.16},
timestamp = {Wed, 07 Feb 2024 14:22:56 +0100},
biburl = {https://dblp.org/rec/conf/csl/BerardiB024.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2401-02091,
author = {Adriano Barile and
Stefano Berardi and
Luca Roversi},
title = {Termination of Rewriting on Reversible Boolean Circuits as a Free
3-Category Problem},
journal = {CoRR},
volume = {abs/2401.02091},
year = {2024},
url = {https://doi.org/10.48550/arXiv.2401.02091},
doi = {10.48550/ARXIV.2401.02091},
eprinttype = {arXiv},
eprint = {2401.02091},
timestamp = {Tue, 23 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2401-02091.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ictcs/BarileBR23,
author = {Adriano Barile and
Stefano Berardi and
Luca Roversi},
editor = {Giuseppa Castiglione and
Marinella Sciortino},
title = {Termination of Rewriting on Reversible Boolean Circuits as a Free
3-Category Problem},
booktitle = {Proceedings of the 24th Italian Conference on Theoretical Computer
Science, Palermo, Italy, September 13-15, 2023},
series = {{CEUR} Workshop Proceedings},
volume = {3587},
pages = {31--43},
publisher = {CEUR-WS.org},
year = {2023},
url = {https://ceur-ws.org/Vol-3587/5208.pdf},
timestamp = {Mon, 18 Dec 2023 16:58:34 +0100},
biburl = {https://dblp.org/rec/conf/ictcs/BarileBR23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/types/2020,
editor = {Ugo de'Liguoro and
Stefano Berardi and
Thorsten Altenkirch},
title = {26th International Conference on Types for Proofs and Programs, {TYPES}
2020, March 2-5, 2020, University of Turin, Italy},
series = {LIPIcs},
volume = {188},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2021},
url = {https://www.dagstuhl.de/dagpub/978-3-95977-182-5},
isbn = {978-3-95977-182-5},
timestamp = {Mon, 07 Jun 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/types/2020.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/lmcs/BerardiT19,
author = {Stefano Berardi and
Makoto Tatsuta},
title = {Classical System of Martin-Lof's Inductive Definitions is not Equivalent
to Cyclic Proofs},
journal = {Log. Methods Comput. Sci.},
volume = {15},
number = {3},
year = {2019},
url = {https://doi.org/10.23638/LMCS-15(3:10)2019},
doi = {10.23638/LMCS-15(3:10)2019},
timestamp = {Thu, 18 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/lmcs/BerardiT19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/logcom/BerardiOS19,
author = {Stefano Berardi and
Paulo Oliva and
Silvia Steila},
title = {An analysis of the Podelski-Rybalchenko termination theorem via bar
recursion},
journal = {J. Log. Comput.},
volume = {29},
number = {4},
pages = {555--575},
year = {2019},
url = {https://doi.org/10.1093/logcom/exv058},
doi = {10.1093/LOGCOM/EXV058},
timestamp = {Mon, 29 Jul 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/logcom/BerardiOS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cmcs/BerardiT18,
author = {Stefano Berardi and
Makoto Tatsuta},
editor = {Corina C{\^{\i}}rstea},
title = {Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between
Inductive Definitions and Cyclic Proofs},
booktitle = {Coalgebraic Methods in Computer Science - 14th {IFIP} {WG} 1.3 International
Workshop, {CMCS} 2018, Colocated with {ETAPS} 2018, Thessaloniki,
Greece, April 14-15, 2018, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {11202},
pages = {13--33},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-030-00389-0\_3},
doi = {10.1007/978-3-030-00389-0\_3},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
biburl = {https://dblp.org/rec/conf/cmcs/BerardiT18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-1810-05392,
editor = {Stefano Berardi and
Alexandre Miquel},
title = {Proceedings Seventh International Workshop on Classical Logic and
Computation, CL{\&}C 2018, Oxford (UK), 7th of July 2018},
series = {{EPTCS}},
volume = {281},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.281},
doi = {10.4204/EPTCS.281},
timestamp = {Tue, 04 Dec 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-1810-05392.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fuin/Berardid17a,
author = {Stefano Berardi and
Ugo de'Liguoro},
title = {Non-monotonic Pre-fix Points and Learning},
journal = {Fundam. Informaticae},
volume = {150},
number = {3-4},
pages = {259--280},
year = {2017},
url = {https://doi.org/10.3233/FI-2017-1470},
doi = {10.3233/FI-2017-1470},
timestamp = {Fri, 18 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/fuin/Berardid17a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/BerardiS17,
author = {Stefano Berardi and
Silvia Steila},
title = {Ramsey's Theorem for Pairs and k Colors as a sub-Classical Principle
of Arithmetic},
journal = {J. Symb. Log.},
volume = {82},
number = {2},
pages = {737--753},
year = {2017},
url = {https://doi.org/10.1017/jsl.2016.41},
doi = {10.1017/JSL.2016.41},
timestamp = {Fri, 30 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jsyml/BerardiS17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fossacs/BerardiT17,
author = {Stefano Berardi and
Makoto Tatsuta},
editor = {Javier Esparza and
Andrzej S. Murawski},
title = {Classical System of Martin-L{\"{o}}f's Inductive Definitions
Is Not Equivalent to Cyclic Proof System},
booktitle = {Foundations of Software Science and Computation Structures - 20th
International Conference, {FOSSACS} 2017, Held as Part of the European
Joint Conferences on Theory and Practice of Software, {ETAPS} 2017,
Uppsala, Sweden, April 22-29, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10203},
pages = {301--317},
year = {2017},
url = {https://doi.org/10.1007/978-3-662-54458-7\_18},
doi = {10.1007/978-3-662-54458-7\_18},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/fossacs/BerardiT17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/BerardiT17,
author = {Stefano Berardi and
Makoto Tatsuta},
title = {Equivalence of inductive definitions and cyclic proofs under arithmetic},
booktitle = {32nd Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
2017, Reykjavik, Iceland, June 20-23, 2017},
pages = {1--12},
publisher = {{IEEE} Computer Society},
year = {2017},
url = {https://doi.org/10.1109/LICS.2017.8005114},
doi = {10.1109/LICS.2017.8005114},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/BerardiT17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1712-03502,
author = {Stefano Berardi and
Makoto Tatsuta},
title = {Equivalence of Intuitionistic Inductive Definitions and Intuitionistic
Cyclic Proofs under Arithmetic},
journal = {CoRR},
volume = {abs/1712.03502},
year = {2017},
url = {http://arxiv.org/abs/1712.03502},
eprinttype = {arXiv},
eprint = {1712.03502},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1712-03502.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1712-09603,
author = {Stefano Berardi and
Makoto Tatsuta},
title = {Classical System of Martin-Lof's Inductive Definitions is not Equivalent
to Cyclic Proofs},
journal = {CoRR},
volume = {abs/1712.09603},
year = {2017},
url = {http://arxiv.org/abs/1712.09603},
eprinttype = {arXiv},
eprint = {1712.09603},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1712-09603.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/KohlenbachBB16,
editor = {Ulrich Kohlenbach and
Steffen van Bakel and
Stefano Berardi},
title = {Proceedings Sixth International Workshop on Classical Logic and Computation,
CL{\&}C 2016, Porto, Portugal , 23th June 2016},
series = {{EPTCS}},
volume = {213},
year = {2016},
url = {https://doi.org/10.4204/EPTCS.213},
doi = {10.4204/EPTCS.213},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/KohlenbachBB16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BerardiS16,
author = {Stefano Berardi and
Silvia Steila},
title = {Ramsey's Theorem for Pairs and {\textdollar}k{\textdollar} Colors
as a Sub-Classical Principle of Arithmetic},
journal = {CoRR},
volume = {abs/1601.01891},
year = {2016},
url = {http://arxiv.org/abs/1601.01891},
eprinttype = {arXiv},
eprint = {1601.01891},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BerardiS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/Berardi16,
author = {Stefano Berardi},
title = {A Sound, Complete and Effective Second Order Game Semantics},
journal = {CoRR},
volume = {abs/1610.08845},
year = {2016},
url = {http://arxiv.org/abs/1610.08845},
eprinttype = {arXiv},
eprint = {1610.08845},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Berardi16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/BerardiS15,
author = {Stefano Berardi and
Silvia Steila},
title = {An intuitionistic version of Ramsey's Theorem and its use in Program
Termination},
journal = {Ann. Pure Appl. Log.},
volume = {166},
number = {12},
pages = {1382--1406},
year = {2015},
url = {https://doi.org/10.1016/j.apal.2015.08.002},
doi = {10.1016/J.APAL.2015.08.002},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/BerardiS15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/Berardi15,
author = {Stefano Berardi},
editor = {Stephan Kreutzer},
title = {Classical and Intuitionistic Arithmetic with Higher Order Comprehension
Coincide on Inductive Well-Foundedness},
booktitle = {24th {EACSL} Annual Conference on Computer Science Logic, {CSL} 2015,
September 7-10, 2015, Berlin, Germany},
series = {LIPIcs},
volume = {41},
pages = {343--358},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2015},
url = {https://doi.org/10.4230/LIPIcs.CSL.2015.343},
doi = {10.4230/LIPICS.CSL.2015.343},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/csl/Berardi15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/Berardid14,
author = {Stefano Berardi and
Ugo de'Liguoro},
title = {Knowledge Spaces and the Completeness of Learning Strategies},
journal = {Log. Methods Comput. Sci.},
volume = {10},
number = {1},
year = {2014},
url = {https://doi.org/10.2168/LMCS-10(1:9)2014},
doi = {10.2168/LMCS-10(1:9)2014},
timestamp = {Thu, 25 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Berardid14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ictcs/BerardiOS14,
author = {Stefano Berardi and
Paulo Oliva and
Silvia Steila},
editor = {Stefano Bistarelli and
Andrea Formisano},
title = {Proving termination of programs having transition invariants of height
{\(\omega\)}},
booktitle = {Proceedings of the 15th Italian Conference on Theoretical Computer
Science, Perugia, Italy, September 17-19, 2014},
series = {{CEUR} Workshop Proceedings},
volume = {1231},
pages = {237--240},
publisher = {CEUR-WS.org},
year = {2014},
url = {https://ceur-ws.org/Vol-1231/short1.pdf},
timestamp = {Fri, 10 Mar 2023 16:23:17 +0100},
biburl = {https://dblp.org/rec/conf/ictcs/BerardiOS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/rta/BerardiS14,
author = {Stefano Berardi and
Silvia Steila},
editor = {Gilles Dowek},
title = {Ramsey Theorem as an Intuitionistic Property of Well Founded Relations},
booktitle = {Rewriting and Typed Lambda Calculi - Joint International Conference,
{RTA-TLCA} 2014, Held as Part of the Vienna Summer of Logic, {VSL}
2014, Vienna, Austria, July 14-17, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8560},
pages = {93--107},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08918-8\_7},
doi = {10.1007/978-3-319-08918-8\_7},
timestamp = {Tue, 14 May 2019 10:00:46 +0200},
biburl = {https://dblp.org/rec/conf/rta/BerardiS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/Berardi14,
author = {Stefano Berardi},
title = {An intuitionistic version of Ramsey Theorem (italian version)},
journal = {CoRR},
volume = {abs/1401.2515},
year = {2014},
url = {http://arxiv.org/abs/1401.2515},
eprinttype = {arXiv},
eprint = {1401.2515},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Berardi14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BerardiOS14,
author = {Stefano Berardi and
Paulo Oliva and
Silvia Steila},
title = {Proving termination with transition invariants of height omega},
journal = {CoRR},
volume = {abs/1407.4692},
year = {2014},
url = {http://arxiv.org/abs/1407.4692},
eprinttype = {arXiv},
eprint = {1407.4692},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BerardiOS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/BakelBB13,
author = {Steffen van Bakel and
Stefano Berardi and
Ulrich Berger},
title = {Preface},
journal = {Ann. Pure Appl. Log.},
volume = {164},
number = {6},
pages = {589--590},
year = {2013},
url = {https://doi.org/10.1016/j.apal.2012.05.001},
doi = {10.1016/J.APAL.2012.05.001},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/BakelBB13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/AschieriBB13,
author = {Federico Aschieri and
Stefano Berardi and
Giovanni Birolo},
editor = {Simona Ronchi Della Rocca},
title = {Realizability and Strong Normalization for a Curry-Howard Interpretation
of {HA} + {EM1}},
booktitle = {Computer Science Logic 2013 {(CSL} 2013), {CSL} 2013, September 2-5,
2013, Torino, Italy},
series = {LIPIcs},
volume = {23},
pages = {45--60},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2013},
url = {https://doi.org/10.4230/LIPIcs.CSL.2013.45},
doi = {10.4230/LIPICS.CSL.2013.45},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/csl/AschieriBB13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/BerardiT13,
author = {Stefano Berardi and
Makoto Tatsuta},
editor = {Masahito Hasegawa},
title = {Games with Sequential Backtracking and Complete Game Semantics for
Subclassical Logics},
booktitle = {Typed Lambda Calculi and Applications, 11th International Conference,
{TLCA} 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7941},
pages = {61--76},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-38946-7\_7},
doi = {10.1007/978-3-642-38946-7\_7},
timestamp = {Sun, 02 Oct 2022 16:16:31 +0200},
biburl = {https://dblp.org/rec/conf/tlca/BerardiT13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/types/BerardiS13,
author = {Stefano Berardi and
Silvia Steila},
editor = {Ralph Matthes and
Aleksy Schubert},
title = {Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic
Arithmetic},
booktitle = {19th International Conference on Types for Proofs and Programs, {TYPES}
2013, April 22-26, 2013, Toulouse, France},
series = {LIPIcs},
volume = {26},
pages = {64--83},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2013},
url = {https://doi.org/10.4230/LIPIcs.TYPES.2013.64},
doi = {10.4230/LIPICS.TYPES.2013.64},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/types/BerardiS13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/Berardid13,
author = {Stefano Berardi and
Ugo de'Liguoro},
editor = {David Baelde and
Arnaud Carayol},
title = {Non-monotonic Pre-fixed Points and Learning},
booktitle = {Proceedings Workshop on Fixed Points in Computer Science, {FICS} 2013,
Turino, Italy, September 1st, 2013},
series = {{EPTCS}},
volume = {126},
pages = {1--10},
year = {2013},
url = {https://doi.org/10.4204/EPTCS.126.1},
doi = {10.4204/EPTCS.126.1},
timestamp = {Wed, 12 Sep 2018 01:05:15 +0200},
biburl = {https://dblp.org/rec/journals/corr/Berardid13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/BerardiT12,
author = {Stefano Berardi and
Makoto Tatsuta},
title = {Internal models of system {F} for decompilation},
journal = {Theor. Comput. Sci.},
volume = {435},
pages = {3--20},
year = {2012},
url = {https://doi.org/10.1016/j.tcs.2012.02.022},
doi = {10.1016/J.TCS.2012.02.022},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tcs/BerardiT12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocl/Berardid12,
author = {Stefano Berardi and
Ugo de'Liguoro},
title = {Interactive Realizers: {A} New Approach to Program Extraction from
Nonconstructive Proofs},
journal = {{ACM} Trans. Comput. Log.},
volume = {13},
number = {2},
pages = {11:1--11:21},
year = {2012},
url = {https://doi.org/10.1145/2159531.2159533},
doi = {10.1145/2159531.2159533},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tocl/Berardid12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/Berardid12,
author = {Stefano Berardi and
Ugo de'Liguoro},
editor = {Patrick C{\'{e}}gielski and
Arnaud Durand},
title = {Knowledge Spaces and the Completeness of Learning Strategies},
booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st
Annual Conference of the EACSL, {CSL} 2012, September 3-6, 2012, Fontainebleau,
France},
series = {LIPIcs},
volume = {16},
pages = {77--91},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2012},
url = {https://doi.org/10.4230/LIPIcs.CSL.2012.77},
doi = {10.4230/LIPICS.CSL.2012.77},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/csl/Berardid12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/TatsutaB11,
author = {Makoto Tatsuta and
Stefano Berardi},
editor = {Marc Bezem},
title = {Non-Commutative Infinitary Peano Arithmetic},
booktitle = {Computer Science Logic, 25th International Workshop / 20th Annual
Conference of the EACSL, {CSL} 2011, September 12-15, 2011, Bergen,
Norway, Proceedings},
series = {LIPIcs},
volume = {12},
pages = {538--552},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2011},
url = {https://doi.org/10.4230/LIPIcs.CSL.2011.538},
doi = {10.4230/LIPICS.CSL.2011.538},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/csl/TatsutaB11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/BerardiCH10,
author = {Stefano Berardi and
Thierry Coquand and
Susumu Hayashi},
title = {Games with 1-backtracking},
journal = {Ann. Pure Appl. Log.},
volume = {161},
number = {10},
pages = {1254--1269},
year = {2010},
url = {https://doi.org/10.1016/j.apal.2010.03.002},
doi = {10.1016/J.APAL.2010.03.002},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/BerardiCH10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/BakelBB10,
author = {Steffen van Bakel and
Stefano Berardi and
Ulrich Berger},
title = {Preface},
journal = {Ann. Pure Appl. Log.},
volume = {161},
number = {11},
pages = {1313--1314},
year = {2010},
url = {https://doi.org/10.1016/j.apal.2010.04.004},
doi = {10.1016/J.APAL.2010.04.004},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/BakelBB10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1007-1785,
author = {Federico Aschieri and
Stefano Berardi},
title = {Interactive Learning-Based Realizability for Heyting Arithmetic with
{EM1}},
journal = {Log. Methods Comput. Sci.},
volume = {6},
number = {3},
year = {2010},
url = {http://arxiv.org/abs/1007.1785},
timestamp = {Thu, 25 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1007-1785.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/flops/BerardiT10,
author = {Stefano Berardi and
Makoto Tatsuta},
editor = {Matthias Blume and
Naoki Kobayashi and
Germ{\'{a}}n Vidal},
title = {Internal Normalization, Compilation and Decompilation for System \emph{F}\({}_{\mbox{bh}}\)},
booktitle = {Functional and Logic Programming, 10th International Symposium, {FLOPS}
2010, Sendai, Japan, April 19-21, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6009},
pages = {207--223},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-12251-4\_16},
doi = {10.1007/978-3-642-12251-4\_16},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/flops/BerardiT10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-1101-5200,
editor = {Steffen van Bakel and
Stefano Berardi and
Ulrich Berger},
title = {Proceedings Third International Workshop on Classical Logic and Computation,
CL{\&}C 2010, Brno, Czech Republic, 21-22 August 2010},
series = {{EPTCS}},
volume = {47},
year = {2010},
url = {https://doi.org/10.4204/EPTCS.47},
doi = {10.4204/EPTCS.47},
timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1101-5200.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1005-2907,
author = {Stefano Berardi and
Ugo de'Liguoro},
title = {Interactive Realizers and Monads},
journal = {CoRR},
volume = {abs/1005.2907},
year = {2010},
url = {http://arxiv.org/abs/1005.2907},
eprinttype = {arXiv},
eprint = {1005.2907},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1005-2907.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/Berardid09,
author = {Stefano Berardi and
Ugo de'Liguoro},
title = {Toward the interpretation of non-constructive reasoning as non-monotonic
learning},
journal = {Inf. Comput.},
volume = {207},
number = {1},
pages = {63--81},
year = {2009},
url = {https://doi.org/10.1016/j.ic.2008.10.003},
doi = {10.1016/J.IC.2008.10.003},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/Berardid09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/AschieriB09,
author = {Federico Aschieri and
Stefano Berardi},
editor = {Pierre{-}Louis Curien},
title = {Interactive Learning-Based Realizability Interpretation for Heyting
Arithmetic with {EM1}},
booktitle = {Typed Lambda Calculi and Applications, 9th International Conference,
{TLCA} 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5608},
pages = {20--34},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02273-9\_4},
doi = {10.1007/978-3-642-02273-9\_4},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/AschieriB09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/types/2008,
editor = {Stefano Berardi and
Ferruccio Damiani and
Ugo de'Liguoro},
title = {Types for Proofs and Programs, International Conference, {TYPES} 2008,
Torino, Italy, March 26-29, 2008, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {5497},
publisher = {Springer},
year = {2009},
url = {https://doi.org/10.1007/978-3-642-02444-3},
doi = {10.1007/978-3-642-02444-3},
isbn = {978-3-642-02443-6},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/types/2008.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/BakelB08,
author = {Steffen van Bakel and
Stefano Berardi},
title = {Preface},
journal = {Ann. Pure Appl. Log.},
volume = {153},
number = {1-3},
pages = {1--2},
year = {2008},
url = {https://doi.org/10.1016/j.apal.2008.01.007},
doi = {10.1016/J.APAL.2008.01.007},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/BakelB08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/BerardiY08,
author = {Stefano Berardi and
Yoriyuki Yamagata},
title = {A sequent calculus for limit computable mathematics},
journal = {Ann. Pure Appl. Log.},
volume = {153},
number = {1-3},
pages = {111--126},
year = {2008},
url = {https://doi.org/10.1016/j.apal.2008.01.006},
doi = {10.1016/J.APAL.2008.01.006},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/BerardiY08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/Berardid08,
author = {Stefano Berardi and
Ugo de'Liguoro},
title = {Calculi, types and applications: Essays in honour of M. Coppo, M.
Dezani-Ciancaglini and S. Ronchi Della Rocca},
journal = {Theor. Comput. Sci.},
volume = {398},
number = {1-3},
pages = {1--11},
year = {2008},
url = {https://doi.org/10.1016/j.tcs.2008.01.018},
doi = {10.1016/J.TCS.2008.01.018},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tcs/Berardid08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/Berardid08,
author = {Stefano Berardi and
Ugo de'Liguoro},
editor = {Michael Kaminski and
Simone Martini},
title = {A Calculus of Realizers for {EM1} Arithmetic (Extended Abstract)},
booktitle = {Computer Science Logic, 22nd International Workshop, {CSL} 2008, 17th
Annual Conference of the EACSL, Bertinoro, Italy, September 16-19,
2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5213},
pages = {215--229},
publisher = {Springer},
year = {2008},
url = {https://doi.org/10.1007/978-3-540-87531-4\_17},
doi = {10.1007/978-3-540-87531-4\_17},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/csl/Berardid08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/aplas/BerardiT07,
author = {Stefano Berardi and
Makoto Tatsuta},
editor = {Zhong Shao},
title = {Positive Arithmetic Without Exchange Is a Subclassical Logic},
booktitle = {Programming Languages and Systems, 5th Asian Symposium, {APLAS} 2007,
Singapore, November 29-December 1, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4807},
pages = {271--285},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-76637-7\_18},
doi = {10.1007/978-3-540-76637-7\_18},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/aplas/BerardiT07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/Berardi07,
author = {Stefano Berardi},
editor = {Simona Ronchi Della Rocca},
title = {Semantics for Intuitionistic Arithmetic Based on Tarski Games with
Retractable Moves},
booktitle = {Typed Lambda Calculi and Applications, 8th International Conference,
{TLCA} 2007, Paris, France, June 26-28, 2007, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {4583},
pages = {23--38},
publisher = {Springer},
year = {2007},
url = {https://doi.org/10.1007/978-3-540-73228-0\_4},
doi = {10.1007/978-3-540-73228-0\_4},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/Berardi07.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/Berardi06,
author = {Stefano Berardi},
title = {Some intuitionistic equivalents of classical principles for degree
2 formulas},
journal = {Ann. Pure Appl. Log.},
volume = {139},
number = {1-3},
pages = {185--200},
year = {2006},
url = {https://doi.org/10.1016/j.apal.2005.04.006},
doi = {10.1016/J.APAL.2005.04.006},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/Berardi06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mscs/Berardi05,
author = {Stefano Berardi},
title = {Classical logic as limit completion},
journal = {Math. Struct. Comput. Sci.},
volume = {15},
number = {1},
pages = {167--200},
year = {2005},
url = {https://doi.org/10.1017/S0960129504004529},
doi = {10.1017/S0960129504004529},
timestamp = {Wed, 01 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mscs/Berardi05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/galop/BerardiCH05,
author = {Stefano Berardi and
Thierry Coquand and
Susumu Hayashi},
editor = {Dan R. Ghica and
Guy McCusker},
title = {Games with 1-backtracking},
booktitle = {1st Workshop on Games for Logic and Programming Languages, GALOP@ETAPS
2005, Edinburgh, UK, 2-3 April 2005},
pages = {210--225},
year = {2005},
timestamp = {Thu, 25 Jun 2020 16:30:03 +0200},
biburl = {https://dblp.org/rec/conf/galop/BerardiCH05.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/BerardiV04,
author = {Stefano Berardi and
Silvio Valentini},
title = {Krivine's intuitionistic proof of classical completeness (for countable
languages)},
journal = {Ann. Pure Appl. Log.},
volume = {129},
number = {1-3},
pages = {93--106},
year = {2004},
url = {https://doi.org/10.1016/j.apal.2004.01.002},
doi = {10.1016/J.APAL.2004.01.002},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/BerardiV04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mlq/Berardi04,
author = {Stefano Berardi},
title = {A generalization of a conservativity theorem for classical versus
intuitionistic arithmetic},
journal = {Math. Log. Q.},
volume = {50},
number = {1},
pages = {41--46},
year = {2004},
url = {https://doi.org/10.1002/malq.200310074},
doi = {10.1002/MALQ.200310074},
timestamp = {Wed, 17 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mlq/Berardi04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/BerardiB04,
author = {Stefano Berardi and
Chantal Berline},
title = {Building continuous webbed models for system {F}},
journal = {Theor. Comput. Sci.},
volume = {315},
number = {1},
pages = {3--34},
year = {2004},
url = {https://doi.org/10.1016/j.tcs.2003.11.011},
doi = {10.1016/J.TCS.2003.11.011},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tcs/BerardiB04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/AkamaBHK04,
author = {Yohji Akama and
Stefano Berardi and
Susumu Hayashi and
Ulrich Kohlenbach},
title = {An Arithmetical Hierarchy of the Law of Excluded Middle and Related
Principles},
booktitle = {19th {IEEE} Symposium on Logic in Computer Science {(LICS} 2004),
14-17 July 2004, Turku, Finland, Proceedings},
pages = {192--201},
publisher = {{IEEE} Computer Society},
year = {2004},
url = {https://doi.org/10.1109/LICS.2004.1319613},
doi = {10.1109/LICS.2004.1319613},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/AkamaBHK04.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/types/2003,
editor = {Stefano Berardi and
Mario Coppo and
Ferruccio Damiani},
title = {Types for Proofs and Programs, International Workshop, {TYPES} 2003,
Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {3085},
publisher = {Springer},
year = {2004},
url = {https://doi.org/10.1007/b98246},
doi = {10.1007/B98246},
isbn = {3-540-22164-6},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/types/2003.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/BarbaneraB03,
author = {Franco Barbanera and
Stefano Berardi},
title = {A full continuous model of polymorphism},
journal = {Theor. Comput. Sci.},
volume = {290},
number = {1},
pages = {407--428},
year = {2003},
url = {https://doi.org/10.1016/S0304-3975(01)00379-6},
doi = {10.1016/S0304-3975(01)00379-6},
timestamp = {Wed, 17 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/tcs/BarbaneraB03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mscs/BerardiB02,
author = {Stefano Berardi and
Chantal Berline},
title = {BetaEta-Complete Models for System {F}},
journal = {Math. Struct. Comput. Sci.},
volume = {12},
number = {6},
pages = {823--874},
year = {2002},
url = {https://doi.org/10.1017/S0960129502003778},
doi = {10.1017/S0960129502003778},
timestamp = {Wed, 01 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mscs/BerardiB02.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/saig/BerardiCDG00,
author = {Stefano Berardi and
Mario Coppo and
Ferruccio Damiani and
Paola Giannini},
editor = {Walid Taha},
title = {Type-Based Useless-Code Elimination for Functional Programs},
booktitle = {Semantics, Applications, and Implementation of Program Generation,
International Workshop {SAIG} 2000, Montreal, Canada, September 20,
2000, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1924},
pages = {172--189},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/3-540-45350-4\_13},
doi = {10.1007/3-540-45350-4\_13},
timestamp = {Tue, 29 Dec 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/saig/BerardiCDG00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/Berardi99,
author = {Stefano Berardi},
title = {Intuitionistic Completeness for First Order Classical Logic},
journal = {J. Symb. Log.},
volume = {64},
number = {1},
pages = {304--312},
year = {1999},
url = {https://doi.org/10.2307/2586766},
doi = {10.2307/2586766},
timestamp = {Sun, 28 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/Berardi99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/Berardid99,
author = {Stefano Berardi and
Ugo de'Liguoro},
editor = {Jean{-}Yves Girard},
title = {Total Functionals and Well-Founded Strategies},
booktitle = {Typed Lambda Calculi and Applications, 4th International Conference,
TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1581},
pages = {54--68},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-48959-2\_6},
doi = {10.1007/3-540-48959-2\_6},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/Berardid99.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/BerardiBC98,
author = {Stefano Berardi and
Marc Bezem and
Thierry Coquand},
title = {On the Computational Content of the Axiom of Choice},
journal = {J. Symb. Log.},
volume = {63},
number = {2},
pages = {600--622},
year = {1998},
url = {https://doi.org/10.2307/2586854},
doi = {10.2307/2586854},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/BerardiBC98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/logcom/BaratellaB98,
author = {Stefano Baratella and
Stefano Berardi},
title = {Approximating Classical Theorems},
journal = {J. Log. Comput.},
volume = {8},
number = {6},
pages = {839--854},
year = {1998},
url = {https://doi.org/10.1093/logcom/8.6.839},
doi = {10.1093/LOGCOM/8.6.839},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/logcom/BaratellaB98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/BerardiB00,
author = {Stefano Berardi and
Chantal Berline},
editor = {Dieter Spreen and
Ralf Greb and
Holger Schulz and
Michel P. Schellekens},
title = {Building continuous webbed models for system {F}},
booktitle = {Workshop on Domains {IV} 1998, Haus Humboldtstein, Remagen-Rolandseck,
Germany, October 2-4, 1998},
series = {Electronic Notes in Theoretical Computer Science},
volume = {35},
pages = {3--33},
publisher = {Elsevier},
year = {1998},
url = {https://doi.org/10.1016/S1571-0661(05)80724-8},
doi = {10.1016/S1571-0661(05)80724-8},
timestamp = {Wed, 30 Nov 2022 10:39:11 +0100},
biburl = {https://dblp.org/rec/journals/entcs/BerardiB00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/aml/BaratellaB97,
author = {Stefano Baratella and
Stefano Berardi},
title = {A parallel game semantics for Linear Logic},
journal = {Arch. Math. Log.},
volume = {36},
number = {3},
pages = {189--217},
year = {1997},
url = {https://doi.org/10.1007/s001530050061},
doi = {10.1007/S001530050061},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/aml/BaratellaB97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/BarbaneraB97,
author = {Franco Barbanera and
Stefano Berardi},
title = {The Simply-Typed Theory of Beta-Conversion has no Maximum Extension},
journal = {Inf. Comput.},
volume = {139},
number = {1},
pages = {57--61},
year = {1997},
url = {https://doi.org/10.1006/inco.1997.2663},
doi = {10.1006/INCO.1997.2663},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/BarbaneraB97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacs/BarbaneraBS97,
author = {Franco Barbanera and
Stefano Berardi and
Massimo Schivalocchi},
editor = {Mart{\'{\i}}n Abadi and
Takayasu Ito},
title = {"Classical" Programming-with-Proofs in lambda\({}_{\mbox{PA}}\)\({}^{\mbox{Sym}}\):
An Analysis of Non-confluence},
booktitle = {Theoretical Aspects of Computer Software, Third International Symposium,
{TACS} '97, Sendai, Japan, September 23-26, 1997, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1281},
pages = {365--390},
publisher = {Springer},
year = {1997},
url = {https://doi.org/10.1007/BFb0014559},
doi = {10.1007/BFB0014559},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/tacs/BarbaneraBS97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/BerardiB97,
author = {Stefano Berardi and
Luca Boerio},
editor = {Philippe de Groote},
title = {Minimum Information Code in a Pure Functional Language with Data Types},
booktitle = {Typed Lambda Calculi and Applications, Third International Conference
on Typed Lambda Calculi and Applications, {TLCA} '97, Nancy, France,
April 2-4, 1997, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1210},
pages = {30--45},
publisher = {Springer},
year = {1997},
url = {https://doi.org/10.1007/3-540-62688-3\_27},
doi = {10.1007/3-540-62688-3\_27},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/BerardiB97.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/BarbaneraB96,
author = {Franco Barbanera and
Stefano Berardi},
title = {A Symmetric Lambda Calculus for Classical Program Extraction},
journal = {Inf. Comput.},
volume = {125},
number = {2},
pages = {103--117},
year = {1996},
url = {https://doi.org/10.1006/inco.1996.0025},
doi = {10.1006/INCO.1996.0025},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/BarbaneraB96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfp/BarbaneraB96,
author = {Franco Barbanera and
Stefano Berardi},
title = {Proof-Irrelevance out of Exluded-Middle and Choice in the Calculus
of Constructions},
journal = {J. Funct. Program.},
volume = {6},
number = {3},
pages = {519--525},
year = {1996},
url = {https://doi.org/10.1017/S0956796800001829},
doi = {10.1017/S0956796800001829},
timestamp = {Sat, 27 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfp/BarbaneraB96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/logcom/Berardi96,
author = {Stefano Berardi},
title = {Pruning Simply Typed Lambda-Terms},
journal = {J. Log. Comput.},
volume = {6},
number = {5},
pages = {663--681},
year = {1996},
url = {https://doi.org/10.1093/logcom/6.5.663},
doi = {10.1093/LOGCOM/6.5.663},
timestamp = {Wed, 17 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/logcom/Berardi96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ndjfl/BarbaneraB96,
author = {Franco Barbanera and
Stefano Berardi},
title = {A Constructive Valuation Semantics for Classical Logic},
journal = {Notre Dame J. Formal Log.},
volume = {37},
number = {3},
pages = {462--482},
year = {1996},
url = {https://doi.org/10.1305/ndjfl/1039886522},
doi = {10.1305/NDJFL/1039886522},
timestamp = {Thu, 21 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/ndjfl/BarbaneraB96.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/types/1995,
editor = {Stefano Berardi and
Mario Coppo},
title = {Types for Proofs and Programs, International Workshop TYPES'95, Torino,
Italy, June 5-8, 1995, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {1158},
publisher = {Springer},
year = {1996},
url = {https://doi.org/10.1007/3-540-61780-9},
doi = {10.1007/3-540-61780-9},
isbn = {3-540-61780-9},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/types/1995.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/BarbaneraB95,
author = {Franco Barbanera and
Stefano Berardi},
title = {A Strong Normalization Result for Classical Logic},
journal = {Ann. Pure Appl. Log.},
volume = {76},
number = {2},
pages = {99--116},
year = {1995},
url = {https://doi.org/10.1016/0168-0072(95)00004-Z},
doi = {10.1016/0168-0072(95)00004-Z},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/BarbaneraB95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/BerardiBC95,
author = {Stefano Berardi and
Marc Bezem and
Thierry Coquand},
editor = {Mariangiola Dezani{-}Ciancaglini and
Gordon D. Plotkin},
title = {A realization of the negative interpretation of the Axiom of Choice},
booktitle = {Typed Lambda Calculi and Applications, Second International Conference
on Typed Lambda Calculi and Applications, {TLCA} '95, Edinburgh, UK,
April 10-12, 1995, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {902},
pages = {47--62},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/BFb0014044},
doi = {10.1007/BFB0014044},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/BerardiBC95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/BerardiB95,
author = {Stefano Berardi and
Luca Boerio},
editor = {Mariangiola Dezani{-}Ciancaglini and
Gordon D. Plotkin},
title = {Using Subtyping in Program Optimization},
booktitle = {Typed Lambda Calculi and Applications, Second International Conference
on Typed Lambda Calculi and Applications, {TLCA} '95, Edinburgh, UK,
April 10-12, 1995, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {902},
pages = {63--77},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/BFb0014045},
doi = {10.1007/BFB0014045},
timestamp = {Wed, 17 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tlca/BerardiB95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacs/BarbaneraB94,
author = {Franco Barbanera and
Stefano Berardi},
editor = {Masami Hagiya and
John C. Mitchell},
title = {A Symmetric Lambda Calculus for "Classical" Program Extraction},
booktitle = {Theoretical Aspects of Computer Software, International Conference
{TACS} '94, Sendai, Japan, April 19-22, 1994, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {789},
pages = {495--515},
publisher = {Springer},
year = {1994},
url = {https://doi.org/10.1007/3-540-57887-0\_112},
doi = {10.1007/3-540-57887-0\_112},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/tacs/BarbaneraB94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mscs/Berardi93,
author = {Stefano Berardi},
title = {An Application of {PER} Models to Program Extraction},
journal = {Math. Struct. Comput. Sci.},
volume = {3},
number = {3},
pages = {309--331},
year = {1993},
url = {https://doi.org/10.1017/S0960129500000244},
doi = {10.1017/S0960129500000244},
timestamp = {Wed, 01 Apr 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/mscs/Berardi93.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tlca/BarbaneraB93,
author = {Franco Barbanera and
Stefano Berardi},
editor = {Marc Bezem and
Jan Friso Groote},
title = {Extracting Constructive Content from Classical Logic via Control-like
Reductions},
booktitle = {Typed Lambda Calculi and Applications, International Conference on
Typed Lambda Calculi and Applications, {TLCA} '93, Utrecht, The Netherlands,
March 16-18, 1993, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {664},
pages = {45--59},
publisher = {Springer},
year = {1993},
url = {https://doi.org/10.1007/BFb0037097},
doi = {10.1007/BFB0037097},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
biburl = {https://dblp.org/rec/conf/tlca/BarbaneraB93.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/caap/BarbaneraB92,
author = {Franco Barbanera and
Stefano Berardi},
editor = {Jean{-}Claude Raoult},
title = {A Constructive Valuation Interpretation for Classical Logic and its
Use in Witness Extraction},
booktitle = {{CAAP} '92, 17th Colloquium on Trees in Algebra and Programming, Rennes,
France, February 26-28, 1992, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {581},
pages = {1--23},
publisher = {Springer},
year = {1992},
url = {https://doi.org/10.1007/3-540-55251-0\_1},
doi = {10.1007/3-540-55251-0\_1},
timestamp = {Tue, 14 May 2019 10:00:44 +0200},
biburl = {https://dblp.org/rec/conf/caap/BarbaneraB92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/Berardi91,
author = {Stefano Berardi},
title = {Retractions on dI-domains as a model for Type:Type},
journal = {Inf. Comput.},
volume = {94},
number = {2},
pages = {204--231},
year = {1991},
url = {https://doi.org/10.1016/0890-5401(91)90038-4},
doi = {10.1016/0890-5401(91)90038-4},
timestamp = {Fri, 12 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/iandc/Berardi91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/Berardi88,
author = {Stefano Berardi},
title = {Equalization of Finite Flowers},
journal = {J. Symb. Log.},
volume = {53},
number = {1},
pages = {105--123},
year = {1988},
url = {https://doi.org/10.1017/S0022481200028966},
doi = {10.1017/S0022481200028966},
timestamp = {Sun, 28 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/Berardi88.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-02-08 23:16 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
