Alberto Carraro - research

Informazioni generali

Alberto Carraro, MsC. Phd. Eng.
DAIS, Università Ca' Foscari Venezia
Stanza 2, via Torino 155
30172 Venezia, Italia

Contatti

posta elettronica:
acarraro at dsi dot unive dot it
telefono: (+39)(0)41 2348421

Articoli a conferenze

  • [CS09] Carraro A. and Salibra A., Reflexive Scott Domains are not complete for the extensional lambda calculus, Proc. 24th Annual IEEE Symposium on Logic In Computer Science, pp. 91-100 (2009).
  • [CS10] Carraro A. and Salibra A., Easy terms are not always simple, Proc. 12th Italian Conference on Theoretical Computer Science (2010).
  • [CES10] Carraro A., Ehrhard T. and Salibra A., Resource combinatory algebras, Proc. 35th International Symposium on Mathematical Foundations of Computer Science, LNCS vol. 6281, pp. 233-245 (2010).
  • [CES10b] Carraro A., Ehrhard T. and Salibra A., Exponentials with infinite multiplicities, Proc. 19th EACSL Annual Conference on Computer Science Logic, LNCS vol. 6247, pp. 170-184 (2010).
  • [BCEM11] Bucciarelli A., Carraro A., Ehrhard T. and Manzonetto G., Full Abstraction for Resource Calculus with Tests, Proc. 20th EACSL Annual Conference on Computer Science Logic, LIPIcs vol. 12, pp. 97-111 (2011).
  • [CS12] Carraro A., Salibra A., On the equational consistency of order-theoretic models of the lambda calculus, Proc. 21st EACSL Annual Conference on Computer Science Logic, LIPIcs vol. 16, pp. 152-166 (2012).
  • [CG13] Carraro A., Guerrieri G., A semantical and operational account of call-by-value solvability, Proc. FOSSACS, LNCS vol 8412, pp. 103-118 (2014).
  • [BC13] Baldan P., Carraro A., Non-interference by unfolding, PETRI NETS 2014. [OUTSTANDING PAPER AWARD]
  • [BBC14] Baldan P., Burato F., Carraro A., Intransitive Non-interference by unfolding, FACS 2014.
  • [BCFS14] Bucciarelli A., Carraro A., Favro G., Salibra A., A graph easy class of mute lambda terms, ICTCS 2014.

Articoli a workshop

  • [BCES09] Bucciarelli A., Carraro A., Ehrhard T. and Salibra A., On linear information systems, Proc. LINEARITY'09, EPTCS vol. 22, pp. 38-48 (2010).
  • [CES12] Carraro A., Ehrhard T., Salibra A., The stack calculus, Proc. 7th Workshop on Logical and Semantic Frameworks, with Application, EPTCS vol. 113, pp. 93-108 (2012).
  • [C12] Carraro A., The untyped stack calculus and Bohm's theorem, The untyped stack calculus and B\"ohm's theorems, with Application, EPTCS vol. 113, pp. 77-92 (2012).
  • [BCS12] Bucciarelli A., Carraro A., Salibra A., Minimal lambda theories by ultraproducts, Proc. 7th Workshop on Logical and Semantic Frameworks, with Application, EPTCS vol. 113, pp. 61-76 (2012).

Articoli in riviste

  • [CS12b] Carraro A., Salibra A., Easy lambda-terms are not always simple, RAIRO - ITA vol. 46(2) (2012).
  • [BCEM12] Bucciarelli A., Carraro A., Ehrhard T. and Manzonetto G., Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion, LMCS vol. 8(4), pp. 1-44 (2012).
  • [CS13] Carraro A., Salibra A., Ordered models of the lambda calculus, LMCS vol. 9(4) (2013).

Tesi

  • [C11] Carraro A., Théories et modèles du lambda calcul pur et avec ressources, Thesi di Dottorato, Université Paris Diderot e Università Ca' Foscari Venezia, (2011).
  • [C07] Carraro A., Models and theories of lambda calculus, Tesi di Laurea Specialistica, Università Ca' Foscari Venezia, (2007).

Drafts

  • [BBC14] Baldan P., Burato F., Carraro A., Intransitive Non-interference by unfolding.

Software

Alcuni commenti

L'articolo [CS09] affronta un caso particolare di un problema ufficialmente proposto alla comunità scientifica nel 1992 (ma aperto dal 1983 per un gruppo di esperti). Questo problema è elencato come al numero 22 della lista TLCA (http://tlca.di.unito.it/opltlca/), un elenco di 22 problemi, per la maggior parte ancora aperti, che sono rilevanti per la comunità scientifica internazionale che fa riferimento alla alla conferenza "Typed Lambda Calculi and Applications" (TLCA).

L'articolo [CS10] risolve il problema 19 della lista TLCA (vedi sopra), irrisolto dal 2002. Diamo una risposta negativa alla seguente domanda posta da Fabio Alessi: dato un arbitrario easy term M, è sempre possibile dare una prova semantica della sua easiness utilizzando modelli a filtro?

 
11