Vai al contenuto| Home page|

   Ti trovi in: HOME »Programmi, progetti e risultati »I progetti »PRIN - Programmi di ricerca di Rilevante Interesse Nazionale»Programma di ricerca
INIZIO_TESTO_DA_INDICIZZARE

PROGRAMMA DI RICERCA 2004

italiano - english
Unità di Ricerca
Programmi di ricerca simili:
Classificazione scientifico-disciplinare
Classificazione brevettuale
Classificazione geografica
Bibliografia
[ABD03] Alessi F. , F. Barbanera, and M. Dezani-Ciancaglini,
Types and computational rules,
In Wollic'03, volume 84 of ENTCS. Elsevier, 2003.

[As01] A. Asperti, L. Padovani, C. Sacerdoti Coen, I.Schena.
Stylesheets and the re-mathematization of Formal Content.
Proceedings of ``Extreme Markup Languages 2001 Conference'', August 12-17, 2001, Montr'eal, Canada.

[As03] A. Asperti, F.Guidi, L.Padovani, C. Sacerdoti Coen, I. Schena.
Mathematical Knowledge Management in HELM.
Annals of Mahtematics and Artificial Intelligence. vol. 38(1) pp. 27-46, 2003.

[AW03] A. Asperti, B.Wegner.
MOWGLI - An Approach to Machine Understandable Representation of the Mathematical Information in Digital Documents.
LNCS 2730 pp. 14-23. Special issue on Electronic Information and Communication in Mathematics. 2003

[BCD83] H. Barendregt, M. Coppo, M. Dezani-Ciancaglini,
A filter lambda model and the completeness of type assignment,
J. Symbolic Logic 48 (1983), p. 931-940

[B] L. Birkedal,
Developing theories of types and computability via realizability,
Electronic Notes in Theoretical Computer Science, 34 (2000), x+280 p.

[BT] Baader F., and C. Tinelli,
Deciding the Word Problem in the Union of Equational Theories.
Information and Computation, 178 (2),346-390, 2002.

[BGT] Baader F., S. Ghilardi, and C. Tinelli,
A New Combination Procedure for the Word Problem that generalizes Fusion Decidability in Modal Logic.
Proceedings of the Second International Joint Conference on Automated
Reasoning (IJCAR 04), Springer Lecture Notes in Artificial Intelligence, to appear (2004).

[CSSV03] T. Coquand, G. Sambin, J. Smith, S. Valentini,
Inductively generated formal topologies,
Ann. Pure Appl. Logic 124 (2003), 71-106

[CR00] A. Carboni, G. Rosolini,
Locally cartesian closed exact completions,
J. Pure Appl. Algebra 154 (2000), 103-116

[CV98] A. Carboni, E.M. Vitale,
Regular and exact completions,
J. Pure Appl. Alg. 125 (1998), 79-117

[DHA03] Dezani-Ciancaglini M. , F. Honsell, and F. Alessi,
A complete characterization of complete intersection-type preorders,
ACM TOCL, 4(1), pp. 120-147, 2003.

[FG] Fiorentini C., and S. Ghilardi,
Combining Word Problems through Rewriting in Categories with Products.
Theoretical Computer Science, 294,

[G] Ghilardi S.,
Model-Theoretic Methods in Combined Constraint Satisfiability.
Journal of Automated Reasoning, in print 2004.

[G1] M. Grandis,
Categorically algebraic foundations for homotopical algebra,
Appl. Categ. Structures 5 (1997), 363-413.

[G2] M. Grandis,
Directed homotopy theory, I. The fundamental category,
Cah. Topol. Géom. Diff. Catég. 44 (2003), 281-316.

[G3] M. Grandis,
Directed combinatorial homology and noncommutative tori(The breaking of symmetries in algebraic topology),
Math. Proc. Cambridge Philos. Soc., to appear.

[HH] P. Hancock, P. Hyvernat,
Interaction, computer science and formal topology,
Ann. Pure Applied Logic, to appear

[HL99] Honsell, F. M. Lenisa,
Semantical analysis of perpetual strategies in lambda-calculus,
Theoret. Comput. Sci. 212 (1999), 183-209

[HP91] G. Huet, G. Plotkin (eds). "Logical Frameworks".
Cambridge University Press. 1991.

[HP93] G. Huet, G. Plotkin (eds). "Logical Environments".
Cambridge University Press. 1993.

[LS1] J. Lambek, P.J. Scott,
Introduction to higher order categorical logic,
Cambridge University Press, 1986

[LS2] P. Lietz, Th. Streicher,
Impredicativity entails untypedness,
submitted to Math.Struct.Comp.Sci.

[M02] M.E.Maietti
Joyal's arithmetic universes via type theory.
Category Theory in Computer Science, Ottawa 2002,
Electronic Notes in Theoretical Computer Science n.69, 2002.

[MV03] M.E. Maietti, S. Valentini,
Exponentiation of Scott formal topologies,
Workshop Domains VI, Electronic Notes in Theoretical Computer
Science (2003)

[MKM03] A. Asperti, B.Buchberger, J.H.Davenport (EDS). 'Mathematical Knowledge Management'. LECTURE NOTES IN COMPUTER SCIENCE vol. 2594, proceedings of the Second International Conference on Mathematical Knowledge Management, MKM 2003. Bertinoro, Italy, February 2003.

[PRR99] Pravato A., S.Ronchi, L.Roversi,
The call-by-value lambda calculus: a semantic investigation,
Math. Struct. Comp. Sci. 9 (1999), 617-650

[RR] Robinson, E.P., Rosolini, G.,
An abstract look at realizability,
in: Computer Science Logic '01, L. Fribourg ed., Lectures Notes in Computer Science, 2142, Springer (2001), p. 173-187

[S] G. Sambin,
Intuitionistic formal spaces, a first communication,
in: Mathematical Logic and Applications, D. Skordev ed., Plenum (1987), p. 187-204

[S03] G. Sambin,
Some points in formal topology,
Theor. Comp. Sci. 305 (2003), 347-408

[S03b] G. Sambin, with the collaboration of S. Gebellato, P. Martin-Loef, V. Capretta,
The basic Picture,
Preprint n. 8, May 2003, Dip. di Matematica P. e A., Univ. of Padova, pp. 1-129

[SVV96] G. Sambin, S. Valentini, P. Virgili,
Constructive domain theory as a branch of intuitionistic pointfree topology, Theoret. Comput. Sci. 159 (1996), 319-341

[V01] S. Valentini,
A Cartesian closed category in Martin-Loef's intuitionistic type theory.
Theoret. Comput. Sci. 290 (2003), 189-219
Parole Chiave
MATEMATICA COSTRUTTIVA; TEORIA DEI TIPI; TEORIA DELLE CATEGORIE; TOPOLOGIA FORMALE

Metodi Costruttivi in Topologia Algebra e Fondamenti dell'Informatica

Università degli Studi di Padova
Abstract
In matematica indebolire le assunzioni facilita l'emergere di strutture e metodi nuovi. Negli ultimi decenni si e' osservato che cio' vale anche riguardo alla fondazione che si assume. L'adozione della logica intuizionistica e' legata all'emergere, tra l'altro, della teoria dei topos negli anni '70. Piu' di recente, l'adozione di una fondazione predicativa ha facilitato l'introduzione di ulteriori novita' e cosi' il costruttivismo ha trovato motivazioni e applicazioni del tutto nuove. La novita' piu' interessante e' il tentativo di sviluppare una nuova matematica in cui ci sia consapevolezza degli strumenti di prova adottati, per valutare il contenuto informativo dei risultati con essi ottenibili.
L'uso di una fondazione piu' debole fa spesso emergere, oltre al contenuto computazionale, anche concetti nuovi e strutture prima nascoste, che portano ad una comprensione teorica piu' profonda e generale, e a strumenti piu' flessibili e affidabili per le applicazioni. Questo e' un modo efficace per dar vita a strutture e metodi di ragionamento ad un tempo nuovi e costruttivi alla nascita.

Lo sviluppo della matematica all'interno della teoria dei tipi di Martin-Loef ha dato luogo ad esempio alla topologia formale. La scelta di una fondazione intuizionistica e predicativa si rivela non una limitazione, ma anzi una fonte di ispirazione che ha portato all'introduzione di nuovi metodi in topologia (definizione/dimostrazione per induzione e per coinduzione) e ha >>>

Coordinatore Scientifico del Programma di Ricerca
Giovanni SAMBIN Università degli Studi di PADOVA
Obiettivo del Programma di Ricerca
Collegare organicamente i metodi costruttivi emersi nei diversi campi della matematica e dell'informatica, svilupparli teoricamente, eventualmente introducendone di nuovi, estendere il campo delle loro applicazioni sono l'obiettivo principale del progetto Metodi Costruttivi in Topologia Algebra e Fondamenti dell'Informatica (d'ora in poi McTafi).
In matematica indebolire le assunzioni spesso facilita l'emergere di nuove strutture e nuovi metodi. Negli ultimi decenni si e' osservato che questo vale anche riguardo alla fondazione che si assume. L'adozione della logica intuizionistica, in cui non vale il principio logico del terzo escluso, e' legata all'emergere, tra le altre cose, della teoria dei topos negli anni 70. Piu' recentemente, l'adozione di una fondazione predicativa, cioe' una teoria degli insiemi in cui non vale l'assioma dell'insieme potenza e si puo' mantenere una concezione di insieme in cui tutti gli elementi sono generati da regole fissate, ha facilitato l'introduzione di ulteriori novita'. In questo modo il costruttivismo - nato storicamente come alternativa alla matematica classica che patisce i paradossi di inizio '900 - ha trovato motivazioni e applicazioni interamente nuove, meno ideologiche, emerse direttamente dalla ricerca.
La novita' piu' interessante e' il tentativo di sviluppare una nuova matematica in cui ci sia consapevolezza degli strumenti di prova adottati, in modo da poter valutare il contenuto informativo dei risultati con >>>

Risultati parziali attesi
- Teorie dei tipi e loro semantica

* Confronto tra la teoria dei tipi di Martin-Loef ed estensioni di questa, e vari tipi di categorie (topos elementari e indebolimenti di questi come [M02]) e studio delle loro proprieta' computazionali. (unita'

Durata
24 mesi
Base di partenza scientifica nazionale o internazionale
I metodi costruttivi e i suoi piu' tipici linguaggi, cioe' la teoria dei tipi e la teoria delle categorie, costitutiscono uno dei ponti interdisciplinari piu' rilevanti tra la matematica e l'informatica (toccando al contempo alcuni importanti aspetti di filosofia della scienza). Questa relazione interessa sia aspetti semantici che sintattici, e copre settori di varia natura che vanno dalla logica alla topologia algebrica alla teoria della realizzabilita', dalla teoria dei domini fino ad aspetti altamente applicativi quali l'estrazione automatica di programmi a partire dalle loro specifiche, o l'automazione del ragionamento formale.
Lo scopo generale del progetto è di esplicitare l'unità di fondo, individuando e sviluppando le strutture comuni, e favorendo la creazione di nuove sinergie. Passati progetti incentrati sullo stessa tema, e gia' finanziati dal Ministero dell'Istruzione, dell'Universita` e della Ricerca hanno dimostrato la fecondita' di questo approccio e la notevole qualita' scientifica del lavoro svolto, che costituisce anche una solida base di partenza per il lavoro futuro.
La metodologia del progetto, che rende possibile e feconda l'interazione tra ricercatori di aree cosi' diverse si basa su tre aspetti fondamentali:
1. connessioni precise e ben note tra i vari campi, già utilizzate da anni nella comunità scientifica;
2. massima autorevolezza scientifica dei partecipanti nel loro campo;
3. pre-esistenti intensi rapporti di >>>