The Logic Group in the Mathematical Department of the University of Padova works mainly on the development of formal topology in a mathematical set theory based on Martin-Loef type theory or its suitable extensions. This approach requires both to study directly formal topology and its applications and type theory as well as more general typed lambda-calculi. In October 1997 the Logic Group organized the "First Workshop on Formal Topology".
Venanzio Capretta, besides his works in collaboration with G.Sambin and S.Valentini, studied the constructive contents of non predicative typed lambda calculi in [Cap96].
Maria Emilia Maietti, besides the works in collaboration with S.Valentini, has been working on the type theories of some categorical universes in [Mai96a], [Mai96b], [Mai98].
Silvia Gebellato and Giovanni Sambin have continued the development of the basic picture, a study of the deep logical structure of a generale notion of space. Particularly novel topics have been formal closed subsets, binary positivity predicate and continuos relations, see [SG97] and [Sam98].
Giovanni Sambin, with Giulia Battilotti and Claudia Faggian, have continued the development of basic logic, recently beginning a study of the associated notion of computation. A new significant conceptual tool has been found in the principle of reflection, originally applied to obtain basic logic, which now seems to have wider applications, also in the field of type theory, see [Bat97], [Bat98], [BF98], [BS95], [Fag98], [FS97] and [SBF98].
Silvio Valentini has been working on typed lambda calculi obtaining both general results, as in [CV97] and [Val98], or more in particular about Martin-Loef's type theory, see for instance [MV96], [SV98], [Val96a] and [Val96b], or in the development of other foundational type theory which can be used as a foundation for intuitionistic mathematic, see for instance [MV98]. Moreover he obtained some results on formal topology, see for instance [V96c] and [Val97]. He collaborates both with Thierry Coquand of the Chalmers University on formal topology, see for instance [CSV97], and with Milena Stefanova of the Nijmegen University on typed lambda calculi and pure type systems, see [MV98].
Paolo Virgili studied the possibility to extend type theory with quotient types in [Vir97].
References
[Bat97] G.Battilotti, "Basic logic through the reflection principle", Diss. Summ. Math., to appear (Summary of the Ph. D. Thesis in italian, University of Siena, 1997, supervisor: G. Sambin).
[Bat98] G.Battilotti, "Embedding classical logic into basic orthologic with a primitive modality", Logic Journal of the IGPL, Special issue on generalized sequent systems, H. Wansing ed., to appear.
[BF98] G.Battilotti and C.Faggian, "Quantum logic and the cube of logics", in Handbook of Philosophical Logic (new edition), vol. VII, D. Gabbay and F. Guenthner eds., Kluwer, to appear.
[BS95] G.Battilotti and G.Sambin, "Basic logic and the cube of its extensions", in Logic in Florence '95, Proceedings of LMPS, Florence 1995, A. Cantini, E. Casari, and P. Minari, eds., Kluwer, to appear.
[Cap96] V.Capretta, "Analisi costruttiva della normalizzazione del system F di Girard", Tesi di Laurea in Matematica, Universita` di Padova, November 1996, advisor: S. Valentini.
[CV97] V.Capretta and S.Valentini, "A general method to prove the normalization theorem for first and second order typed lambda-calculi", to apper in Mathematical structures in computer science.
[CSV97] T.Coquand, G.Sambin, and S.Valentini, "Inductive generation of formal topologies", first draft, 1997.
[Fag98] C.Faggian, "Classical proofs via basic logic", in Proceedings of CSL '97, Aarhus, M. Nielsen and W. Thomas eds., Lecture Notes in Computer Science, Springer, to appear.
[FS97] C.Faggian and G.Sambin, "From basic logic to quantum logics with cut elimination", in Proceedings of the International Quantum Structures Association Berlin '96, special issue of International Journal of Theoretical Physics, vol. 12, 1997.
[MV96] D.Maguolo and S.Valentini, "An intuitionistic version of Cantor's theorem", Mathematical Logic Quarterly, 42 (1996), pp. 446-448.
[Mai96a] M.E.Maietti, "Some aspects of the categorical semantics for the polymorphic lambda calculus", in Logic and Algebra, A.Ursini and P.Agliano`, eds., vol.180 of Lecture Notes in Pure and Applied Mathematics, New York, 1996, Dekker, pp. 589-601.
[Mai96b] M.E.Maietti, "The internal type theory of a Heyting pretopos", to appear in: Types '96, Proceedings of the Annual Meeting of the Types Working Group, Assuois, December 15 -19, 1996.
[Mai98] M.E.Maietti, "The type theory of categorical universes", 1998, Tesi di Dottorato, in preparation, supervisor: S. Valentini.
[MV98] M.E.Maietti and S.Valentini, "Why you should not add powerset to Martin-Loef's intuitionistic type theory", to appear.
[Sam98] G.Sambin, "The basic picture I: the structure underlying topology", 1997, first draft of a comunication presented at the first workshop on Formal Topology, Padova, October 1997.
[SBF98] G.Sambin, G.Battilotti, and C.Faggian, "Basic logic: reflection, symmetry, visibility", Journal of Symbolic Logic, to appear.
[SG97] G.Sambin and S.Gebellato, "A preview of the basic picture, a new trend in formal topology", 1997, Presented at Types'96, Aussois, December 1996, to appear.
[SV98] G.Sambin and S.Valentini, "Building up a toolbox for Martin-Loef's type theory: subset theory", in Twenty-five years of constructive type theory, Proceedings of the Congress held in Venice, October 19-21, 1995, G.Sambin and J.Smith, eds., Oxford U. P., 1998.
[SV97] M.Stefanova, S.Valentini, "A new proof of consistency for Girard's System F", first draft,1997.
[Val96a] S.Valentini, "Decidability in intuitionistic theory of types is functionally decidable", Mathematical Logic Quarterly, 42 (1996), pp. 300-304.
[Val96b] S.Valentini, "The formal development of non-trivial programs in constructive type theory", in Atti del congresso MPC96, Ischia, Maggio, 1996.
[Val96c] S.Valentini, "A completeness theorem for formal topologies", in Logic and Algebra, A.Ursini and P.Agliano`, eds., New York, 1996, Marcel Dekker, pp. 689-702.
[Val97] S.Valentini, "On the formal points of the formal topology of the binary tree", first draft of a comunication presented at the first workshop on Formal Topology, Padova, October 1997.
[Val98] S.Valentini, "The forget-restore principle: a paradigmatic example", in Twenty-five years of constructive type theory, Proceedings of the Congress held in Venice, October 19-21, 1995, G.Sambin and J.Smith, eds., Oxford U.P., 1998.
[Vir97] P.Virgili, "Quozienti in teoria dei tipi di Martin-Loef". Tesi di dottorato, February 1997, supervisor: S. Valentini.