Stefano Berardi - Research: Curriculum, Papers, Ph.d.Thesis, Talks, Technical Reports

``Semantics and Logics of Computation'' group (University of Turin)

Stefano Berardi: Curriculum vitae
Last Update: October, 16, 2007. Home page of the author at C.S.Dept of Turin University.

Born in Torino, January 5, 1962. Assistent Professor at C.S. Dept. of Turin University since November 1, 1990. Associate professor since November, 1 1998, Full Professor since October 1, 2001. His Ph.d. thesis is quoted in the "Handbook of Logic in Computer Science" by H. Barendregt as a basic contribution toward a systematic understanding of typed lambda calculi. Member of Esprit Projects "Logical Frameworks" (1989-91), and "Types for Proofs and Programs" (1992-2007). Organizer of two congresses of this project (in 1995 and in 2004), and Editor of the proceedings (LNCS 1158, LNCS 3085). Editor of special issues of TCS, APAL, Fundamenda Informaticae to appear. Research topics: typed lambda calculi, control operators, computer-aided developing of formal proofs, program extraction from proofs, computational content of classical logic.
List of papers of Stefano Berardi ``THE

``Semantics and Logics of Computation'' group (University of Turin)

Stefano Berardi: Publications

Last Update: May, 2001. Home page of the author.

Riviste internazionali:

(1) "Equalization of Finite Flowers", S.Berardi. Journal of Symbolic Logic, Marzo 1988, Volume 53.
(2) "On the Constructive Content of the Axiom of Choice." S. Berardi, M. Bezem, T. Coquand. In corso di pubblicazione su: J.S.L..
(3) "Intuitionistic Completness for First Order Classical Logic" S. Berardi In corso di pubblicazione su: J.S.L..
(4) "A Strong Normalization Result for Classical Logic" F. Barbanera, S. Berardi. Annals of Pure and Applied Logic. Vol. 76 Pag. 99-116, 1995.
(5) "dI domains as a model for lambda-beta-p and higher order functional languages", S. Berardi. Information and Computation, Vol. 94, No. 2, October 1991.
(6) "A Symmetric Lambda-Calculus for ``Classical'' Program Extraction", F. Barbanera, S. Berardi. Information and Computation, Vol.125, No.2, March 15, 1996.
(7) "There is no maximal equational theory for lambda->", F. Barbanera, S. Berardi. In corso di pubblicazione su: Information and Computation.
(8) "Pruning Simply Typed Lambda Terms" (MacWord file). S. Berardi. Journal of Logic and Computation, Vol.6 No 5, pp663-681 1996. Extended version available (MacWord file).
(9) "An application of PER model to Program Extraction", S. Berardi. Mathematical Structures in Computer Science, 1993, vol. 3, pp. 309-331.
(10) "A Parallel Game Semantic for Linear Logic" S. Baratella, S. Berardi. In corso di pubblicazione su: Archive for Math. Log..
(11) "Proof-irrelevance out of Excluded Middle and Choice in the Calculus of Constructions." F. Barbanera, S. Berardi. Journal of Functional Programming, vol.6(3), 519-525, 1996.
(12) A Constructive Valuation Semantic for Classical Logic, Franco Barbanera, Stefano Berardi Notre Dame Journal of Formal Logic, vol.37, No.3, 462-482, 1996.
(13) Approximating Classical Theorems, Stefano Baratella, Stefano Berardi, Journal of Logic and Computation, to appear.

Atti di congressi internazionali:

(1) "Witness extraction through normalization" F. Barbanera, S. Berardi. Edinburgh BRA conference "Logical Frameworks", in "Logical Environments", edito da G.Huet and G.Plotkin, Cambridge University Press, 1993.
(2) "Encoding of Data Types in Pure Construction Calculus: a semantic justification" S. Berardi. Edinburgh BRA conference "Logical Frameworks", in "Logical Environments", edito da G.Huet and G.Plotkin, Cambridge University Press, 1993.
(3) "Yet Another Constructivization of Classical logic". S. Baratella, S. Berardi, in "Twenty-five years of Constructive Type Theory", edito da G. Sambin e J. Smith, Oxford Press.
(4) "On the Constructive Content of the Axiom of Choice." S. Berardi, M. Bezem, T. Coquand. Proceedings TLCA95, Edinburgh, su: LNCS 902.
(5) "Extracting Constructive Content from Classical Logic via Control-like Reductions". S. Berardi, F. Barbanera. Proceedings of TLCA'93, Utrecht, su: M. Bezem, J.F.Groote eds, LNCS 664, 1993
(6) "A symmetric lambda calculus for ``Classical'' Program Extraction", S. Berardi, F. Barbanera. Proceedings of TACS '94, Sendai, Japan, su: LNCS 789, Springer Verlag, 1994.
(7) "Minimum Information Code in a Pure Functional Language with Data Types." S. Berardi, L. Boerio. TLCA 97, Nancy, France, in corso di pubblicazione su LNCS.
(8) "A constructive valuation interpretation for Classical Logic and its use in Witness extraction", F. Barbanera, S. Berardi. CAAP '92, su LNCS 581, pp.1-12.
(9) "Classical" Programming-with-Proofs in lambda_sym: An Analysis of Non-Confluence" Franco Barbanera, Stefano Berardi, Massimo Schivalocchi Proceedings of TACS '97, Japan, in corso di pubblicazione su LNCS.
(10) "Using Subtyping In Program Optimization." S. Berardi, L. Boerio. Proceedings TLCA95, Edinburgh, su: LNCS 902.

Pubblicazioni italiane.

(1) "A Semantic Purely Intuitionistic Proof of Takeuti's Conjecture", Rendiconti del Seminario Matematico dell'Universita' e del Politecnico di Torino, Fascicolo 46, 1. Aprile 1988.
(2) "Type Dependence and Constructive Mathematics" , Tesi di dottorato di S. Berardi, Torino, 1989.
(3) "Analogie Strutturali ...", S. Berardi, tesi di laurea, pubblicata sul quaderno di Matematica n.94 dell'Universita' di Torino.

Stefano Berardi: technical reports, Ph. thesis supervised. ``THE

``Semantics and Logics of Computation'' group (University of Turin)

Stefano Berardi: Ph.d. thesis supervised, Talks, Technical Reports.

Last Update: February 1998. Home page of the author.

Ph.d. thesis

Ph.d. thesis of L. Boerio, "Optimizing Programs Extracted From Proofs" , Torino, C.S. Dept., 1995.
Ph.d. thesis of F.Barbanera "The witness ..." Torino, C.S. Dept., 1993 (?).
Ph.d. thesis of J.Ekman, Normal proof in set theory. Goteborg, C.S. Dept., 1994.
Ph.d. thesis of T. Altenkirch, Constructions, Inductive Types and Strong Normalization. Edinburgh, C.S. Dept., 1993.
Ph.d. thesis of H.Herbelin "Sequents qu'on calcule" . Paris VII, U.E.R. Math.Informatique, 1995.
Ph.d. thesis of N.Szasz, A Theory of Specifications, Programs and Proofs. Goteborg, C.S. Dept., 1996.

Talks (only those in PowerPoint format)

Program Transformation

Transfinite games

Techical Reports (page under construction).

Stefano Berardi, "Pruning Simply Typed Lambda Terms (full version, MacWord)" , Torino, C.S. Dept., 1997. Condensed version available (MacWord) . Note about pruning algorithm (rtf) .
Stefano Berardi, "Krivine's Intuitionistic Completeness Proof for Classical Logic" , Torino, C.S. Dept., 1997.
Stefano Baratella, Stefano Berardi, "Costruttivizzazione della continuita' Uniforme." 1 , 2 , 3 , Torino, C.S. Dept., February 1998.
Stefano Berardi, Ugo de' Liguoro, "Non-controesempio e Taglio n. 0 , 1 , 2 , 3 , 4 , 5 , 6 , 7 , Torino, C.S. Dept., 1998.
Viviana Patti, "Sintesi di Programmi da Prove costruttive" , Torino, C.S. Dept., 1998.
Stefano Berardi, "Un'analisi della Gerarchia Veloce di funzioni ricorsive" , Torino, C.S. Dept., 1998.
Stefano Berardi, Chantal Berline Beta-eta-complete models for System F, preprint 35 p., submitted (format: gzipped dvi or ps . Torino, C.S. Dept., 1998.
Stefano Berardi, U. de' Liguoro "Total Functionals and Well-founded Strategies" submitted to TLCA99 (format: dvi or gzipped ps ) Torino, C.S. Dept., 1998.
Stefano Berardi, T. Coquand "Transfinite Games", preliminary version (format: gzipped ps , or dvi ) Torino, C.S. Dept., 1996. Version for pubblication: Torino, 1998 (format: gzipped ps , or dvi ). Short note: "A conjecture for Game Theory" (preliminary version, format: rtf ).