RICERCA ITALIANA     

Programmi di ricerca simili:

• 1 - Controllo e certificazione dell'uso delle risorse (CONCERTO)
• 2 - Logiche a più valori e informazione incerta: metodologie algebriche e algoritmiche.
• 3 - 'Mathesis Universalis', oggetti astratti e processi formali.
• 4 - Fondamenti Logici dei Sistemi Distribuiti e Codice Mobile
• 5 - Sistemi a oggetti estendibili per ambienti dinamici e impredicibili (EOS DUE)
• 6 - Aspetti matematici e applicazioni emergenti degli automi e dei linguaggi formali
• 7 - Metodi Costruttivi in Topologia Algebra e Fondamenti dell'Informatica
• 8 - Sistemi ad oggetti estendibili (EOS)
• 9 - Automi e Linguaggi Formali: aspetti matematici e applicativi
• 10 - MODELLI, STRATEGIE E RAPPRESENTAZIONI NELL' EPISTEMOLOGIA DELLA RICERCA SCIENTIFICA

Classificazione scientifico-disciplinare

• Area scientifico disciplinare: Scienze matematiche e informatiche
  • INFORMATICA
  • LOGICA MATEMATICA

Classificazione brevettuale

• PHYSICS
  • COMPUTING; CALCULATING; COUNTING (score computers for games A63; combinations of writing applicances with computing devices B43K29/08)
    • COMPUTER SYSTEMS BASED ON SPECIFIC COMPUTATIONAL MODELS [N0004]
    • ELECTRICAL DIGITAL DATA PROCESSING (computers in which a part of the computation is effected hydraulically or pneumatically G06D; optically G06E; self-contained input or output peripheral equipment G06K; impedance networks using digital techniques H03H) [C9603]

Classificazione geografica

• Regione: Piemonte

Bibliografia

[1] S. Abramsky, P. Malacaria, and R. Jagadeesan. Full abstraction for PCF.
IC, 163:409–470, 2000.
[2] V.M. Abrusci. Noncommutative proof nets. In Adv. in lin. logic (222).
Cambridge Univ. Press, 1995.
[3] V.M. Abrusci and P. Ruet. Non-commutative logic. I. The multiplicative
fragment. Ann. Pure Appl. Logic, 101:29–64, 2000.
[4] F. Alessi, M. Dezani-Ciancaglini, and F. Honsell. Filter models and easy
terms. In ICTCS, LNCS(2202:17-37), 2001.
[5] J.M. Andreoli. Focussing and proof construction. Ann. Pure Appl. Logic,
107:131–163, 2001.
[6] J.M. Andreoli, R. Maieli, and P. Ruet. Constraint-based proof construction
in non commutative logic. TCS, 2004. To appear.
[7] A. Asperti. Linear logic, comonads and optimal reduction. Fund. Inform.,
22:3–22, 1995.
[8] A. Asperti, P. Coppola, and S. Martini. (Optimal) duplication is not elementary
recursive. In 27th SIGPLAN-SIGACT, pages 96–107. ACM, 2000.
[9] A. Asperti and S. Guerrini. The optimal Implementation of Functional
Programming Languages. Cambridge Tracts in TCS, 45. Cambridge Univ.
Press, 1998.
[10] A. Asperti and L. Roversi. Intuitionistic light affine logic. ACM Trans. on
Comp. Logic, 3:1–39, 2002.
[11] P. Baillot. Type inference for polynomial time complexity via constraints
on words. TCS, 2004. To appear.
[12] S. Bellantoni and S. Cook. A new recursion-theoretic characterization of
the polytime functions. Comp. Compl., 2:97–110, 1992.
[13] G. Bellin. Subnets of proof-nets in multiplicative linear logic with MIX.
MSCS, 7:663–699, 1997.
[14] G. Bellin. Two paradigms of logical computation in affine logic? In Logic
for Concurrency and Synchronisation, 18:115-150. Kluwer Academic, 2003.
[15] N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for
intuitionistic linear logic. InTLCA. LNCS, 664:75-90, 1993.
[16] A. Berarducci and B. Intrigila. Church-rosser -theories, infinite -terms
and consistency problems. In Logic Colloquium ’93. Oxford Univ. Press,
1996.
[17] A. Bucciarelli and T. Ehrhard. Sequentiality in an extensional framework.
IC, 110:265–296, 1994.
[18] A. Bucciarelli and A. Salibra. The minimal graph model of lambda calculus.
In 28th Inter. Symp. on Math. Found. of CS, LNCS, 2747:300-307, 2003.
[19] B. Capitani, M. Loreti, and B. Venneri. Hyperformulae, parallel deductions
and intersection types. ENTCS, 50, 2001.
[20] P. Coppola and S. Martini. Typing lambda terms in elementary logic with
linear constraints. In 5th TLCA, LNCS, 2044:76-90, 2001.
[21] P. Coppola and S. Ronchi della Rocca. Principal Typing in Elementary
Affine Logic. In 7th TLCA, LNCS, 2701:90-104, 2003.
[22] U. Dal Lago. On the expressive power of light affine logic. In 8th ICTCS,
LNCS, 2841:216-227, 2003.
[23] U. Dal Lago and S. Martini. Phase semantics and decidability of elementary
affine logic. TCS, 2004. To appear.
[24] U. Dal Lago, S. Martini, and L. Roversi. Higher-order linear ramified
recurrence. In 3th Types for Proofs and Programs, LNCS, 2004. to appear.
[25] V. Danos, J.B. Joinet, and H. Schellinx. A new deconstructive logic: classical
logic. JSL, 62:755–807, 1997.
[26] J.Y. Girard. Linear logic. TCS, 50:1–102, 1987.
[27] J.Y. Girard. Multiplicatives. Rend. Sem. Mat. Univ. Politec. Torino, pages
11–33, 1987. Conf. on Logic and CS: New Trends and Appl.
[28] J.Y. Girard. A new constructive logic : Classical logic. MSCS, 1:255–296,
1991.
[29] J.Y. Girard. Proof-nets: the parallel syntax for proof-theory. In Logic and
algebra, Lect. Notes in Pure and Appl. Math. 180:97-124, 1996.
[30] J.Y. Girard. Light linear logic. IC, 143:175–204, 1998.
[31] J.Y. Girard. Locus solum: from the rules of logics to the logics of rules.
MSCS, 11:301–506, 2001.
[32] G. Gonthier, M. Abadi, and J.J. L`evy. The geometry of optimal lambda
reduction. In 9th SIGPLAN-SIGACT, pages 15–26, 1992.
[33] S. Guerrini, S. Martini, and A. Masini. Proof nets, garbage, and computations.
TCS, 253:185–237, 2001.
[34] M. Hofmann. A mixed modal/linear lambda calculus with applications to
bellantoni-cook safe recursion. In 11th CSL, pages 275–294, 1997.
[35] M. Hofmann. Safe recursion with higher types and BCK-algebra. Ann.
Pure Appl. Logic, 104:113–166, 2000.
[36] M. Hofmann. A type system for bounded space and functional inplaceupdate–
extended abstract. LNCS, 1782, 2000.
[37] F. Honsell and S. Ronchi Della Rocca. An approximation theorem for
topological lambda models and the topological incompleteness of lambda
calculus. J. Comp. and System Sciences, 45:49–75, 1992.
[38] D. Huges and R. Van Glabbeek. Proof nets for unit-free multiplicativeadditive
linear logic. In LICS. IEEE, 2003.
[39] M. Hyland and L.C.H. Ong. On full abstraction for pcf. IC, 163:285–408,
2000.
[40] M. Hyland and A. Schalk. Games on graph and sequentially realizable
functionals. In LICS’02, pages 257–264. IEEE, 2002.
[41] M. Kanovich, M. Okada, and A. Scedrov. Phase semantics for light linear
logic. TCS, 294:525–549, 2003.
[42] Z. Khasidashvili and A. Piperno. A syntactical analysis of normalization.
JLC, 10:381–410, 2000. Type theory and term rewriting.
[43] N. Kobayashi. Quasi-linear types. In 26th SIGPLAN-SIGACT, pages 29–
42, 1999.
[44] Y. Lafont. Soft linear logic and polynomial time. To appear inTCS, 2001.
[45] J. Lamping. An algorithm for optimal lambda calculus reduction. In
Popl’90, pages 16–30, 1990.
[46] O. Laurent. Polarized proof-nets: proof-nets for LC. In TLCA.
LNCS1581:213-227, 1999.
[47] D. Leivant. Stratified functional programs and computational complexity.
In 20th ACM Symp. on Prin. of Prog. Lang., pages 325–333, 1993.
[48] D. Leivant. Ramified recurrence and computational complexity III: Higher
type recurrence and elementary complexity. Ann. Pure Appl. Logic, 96:209–
229, 1999.
[49] J. Longley. The sequentially realizable functionals. Ann. Pure Appl. Logic,
117:1–93, 2002.
[50] R. Maieli and Q. Puite. Modularity of proof-nets: generating the type of a
module. Arch. Math. Logic, 2004. To appear.
[51] P. Neergaard and H. Mairson. LAL is square: Representation and expressiveness
in light affine logic. In 4th ICC, 2002.
[52] L. Paolini and S. Ronchi Della Rocca. Lazy logical semantics. In Cometa’03.
ENTCS, 2003.
[53] L. Paolini and S. Ronchi Della Rocca. Parametric parameter passing
lambda-calculus. IC, 189:87–106, 2004.
[54] M. Parigot. µ-calculus: an algorithmic interpretation of classical natural
deduction. In Logic programming and automated reasoning. LNCS, 624:190-
201, 1992.
[55] M. Pedicini and F. Quaglia. A parallel implementation for optimal lambdacalculus
reduction. In Ppdp 2000, pages 3–14, 2000.
[56] M. Pedicini and F. Quaglia. Scheduling vs communication in pelcr. In
Euro-par 2002, pages 648–655, 2002.
[57] A. Piperno. Normalization and extensionality. In LICS, pages 300–310.
IEEE, 1995.
[58] G. Plotkin. LCF considered as a programming language. TCS, 5:225–255,
1977.
[59] E. Robinson. Proof nets for classical logic. JLC, 13:777–797, 2003.
[60] S. Ronchi Della Rocca. Typed intersection lambda calculus. ENTCS, 70,
2002.
[61] S. Ronchi Della Rocca and L. Roversi. Lambda calculus and intuitionistic
linear logic. Studia Logica, 59:417–448, 1997.
[62] Simona Ronchi Della Rocca and Luca Roversi. Intersection Logic. In CSL.
LNCS, 2412:414-428, 2001.
[63] A. Salibra. Topological incompleteness and order incompleteness of the
lambda calculus. ACM Trans. on Comp. Logic, 4:379–401, 2003. 16th
LICS.
[64] K. Terui. Light affine calculus and polytime strong normalization. In 16th
LICS, pages 209–220. IEEE, 2001.
[65] D. Turner and P. Wadler. Operational interpretations of linear logic. TCS,
227:231–248, 1999.
[66] C. Urban and G.M. Bierman. Strong normalization of cut-elimination in
classical logic. Fund. Inform., 20:1–32, 2000.
[67] D. N. Yetter. Quantales and (noncommutative) linear logic. JSL, 55:41–64,
1990.

Parole Chiave

LOGICA LINEARE; LOGICHE LEGGERE; LINGUAGGI PARADIGMATICI; LAMBDA CALCOLO; COMPLESSITA' COMPUTAZIONALE; TEORIA DELLA DIMOSTRAZIONE; RIDUZIONE OTTIMALE; INTERAZIONE; MODELLI INTENSIONALI ED ESTENSIONALI