Team CARTE

Equipe Associée CRISTAL

CRISTAL ( Contrôle des Ressources par Interprétations Sémantiques et Théorie de la démonstrAtion Linéaire) is an INRIA associated team (équipe associée). The associated team CRISTAL merges italian researchers (from Dipartimento di Informatica, Universita di Torino) and french researchers from INRIA EPI Carte (Loria, Nancy). CRISTAL is financed by INRIA and formalizes the collaboration between these two teams on the topic of resource control using semantics interpretations and linear proof theory.

Members, EPI Carte

Members, Formal Methods in Computing, Dipartimento di informatica, Universita degli Studi di Torino

 

Documents:

Projet proposal

Activity report 2010

Final report 2012

 

Exchanges and collaborations between members of EA CRISTAL:

 

2010:

  • Simona Ronchi Della Rocca, Luca Roversi, Guillaume Bonfante and Romain Péchoux attended a workshop on Implicit Computational Complexity the 23-24 february at the LORIA, organized by EPI Calligramme.
  • Marco Gaboardi visited EPI CARTE from 8 to 12 march.
  • Guillaume Bonfante, Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca, Luca Roversi and Luca Vercelli attended the workshop DICE 2010 (ETAPS affiliated workshop) the 27 and 28 march 2010.
  • Simona Rochi Della Rocca attended the conference FOSSACS 2010 (march 2010).
  • Romain Péchoux has worked with Marco Gaboardi at Universita di Bologna from 10 to 17 april.
  • Jean-Yves Marion was invited by Torino team at a workshop on implicit complexity the 11-13 june.
  • Marco Gaboardi has been to summer school on Logic, Languages, Compilation, and Verification organized by Oregon University.
  • Simona Ronchi Della Rocca, Marco Gaboardi, Guillaume Bonfante and Romain Péchoux attended the workshop LCC (LICS affiliated workshop) in Edinburgh.
  • Marco Gaboardi has visited EPI CARTE from 10 to 17 october 2010.
  • Hugo Férée and Romain Péchoux attended to ISAAC 2010 conference, Jeju island, South Korea.

2011:

  • Luca Roversi visited EPI Carte in Nancy in January 2011.
  • Simona Ronchi Della Rocca, Mauro Piccolo and Marco Gaboardi have visited EPI Carte in Nancy from 4/02/2011 to 13/02/2011.
  • Simona Ronchi Della Rocca, Marco Gaboardi, Luca Roversi and Jean-Yves Marion attended workshop DICE 2011, Saarbrucken, Germany (ETAPS affiliated workshop) the 2 and 3 april 2011.
  • Marco Gaboardi has visited EPI Carte in Nancy in april 2011.
  • Jean-Yves Marion attended LICS 2011 conference (juin 2011, USA).
  • Romain Péchoux has visited Marco Gaboardi at Pennsylvania University (U.Penn), USA, from 17 to 23 august 2011.
  • Marco Gaboardi, Simona Ronchi Della Rocca and Luca Roversi attended to ICFP 2011 conference (September 2011, Japan).

2012:

  • Marco Gaboardi has visited the EPI Carte, from 19 to 23 of March 2012 and from 23 to 27 of April 2012.
  • Romain Péchoux has visited Marco Gaboardi at Pennsylvania University (U.Penn), USA, from 19 to 26 of February 2012 and was invited to give a talk at the Programming languages seminar (PLClub) the 24th of february.
  • Erika De Benedetti, Simona Ronchi Della Rocca and Jean-Yves Marion attended to FOSSACS 2012 and DICE 2012 in Tallin, Estonia, from 31/03/2012 to 1/04/2012.
  • Erika De Benedetti attended to ITRS, Dubrovnik, Croatia the 29th of June 2012.
  • Simona Ronchi Della Rocca attended to CSL 2012, Fontainebleau, from the 3/09/2012 to the 6/09/2012.
  • Romain Péchoux has visited Marco Gaboardi at Pennsylvania University (U.Penn), USA, from 12 to 19 august 2012.
  • From the 29 of October to the 2 of November, Marco Gaboardi will visit and expose some of the EA team results at CMU.

 

Workshop, seminars and scientific events involving members of EA CRISTAL:

2009-2010:

  • Workshop organized by Inria project Calligramme, Loria, Nancy, to which Luca Roversi, Simona Ronchi Della Rocca, Guillaume Bonfante and Romain Péchoux attended.
  • Jean-Yves Marion was member of the program committee of FOPARA 2009, Eindhoven, Netherland (FM affiliated workshop).
  • Jean-Yves Marion and Simona Ronchi Della Rocca were members of the program committee of DICE 2010, Cyprus (ETAPS affiliated workshop).
  • Simona Ronchi Della Rocca was member of the program committee of LCC 2010, Edimburgh, UK (LICS affiliated workshop).

2011:

  • Organization of DICE 2011, ETAPS affiliated workshop. The proceedings are published in EPTCS.
  • Invitation of Daniel Leivant in Carte team, Nancy, from September 2011 to July 2012.
  • Jean-Yves Marion and Luca Roversi were members of the program committee of DICE 2011, Saarbrucken, Germany (ETAPS affiliated workshop).
  • Luca Roversi and Guillaume Bonfante were members of the program committee of LCC 2011, Toronto, Canada (LICS affiliated workshop).
  • Jean-Yves Marion and and Simona Ronchi Della Rocca were members of the program committee of FOPARA 2011, Madrid, Spain.

2012:

  • Edition of a special issue of Information & Computation by J.Y. Marion.
  • Guillaume Bonfante, Marco Gaboardi and Simona Ronchi Della Rocca were members of program committee of DICE 2012, Tallin, Estonia (ETAPS affiliated workshop).

 

 

 

Publications :

2009-2010:

  • Patrick Baillot, Marco Gaboardi, and Virgile Mogbil. A polytime functional language from light linear logic. In ESOP, volume 6012 of LNCS, pages 104–124. Springer, 2010.
  • Ugo Dal Lago, Luca Roversi, and Luca Vercelli. Taming Modal Impredicativity: Superlazy Reduction. In Proceedings of Logical Foundations of Computer Science (LFCS09), volume LNCS 5407 of LNCS, pages 137 – 151. Springer, 2009.
  • Hugo Férée, Emmanuel Hainry, Mathieu Hoyrup, and Romain Péchoux. Interpretation of stream programs: characterizing type 2 polynomial time complexity. pages 291–303. Springer, 2010.
  • Marco Gaboardi, Simona Ronchi Della Rocca, and Jean-Yves Marion. A Logical Account of PSPACE. 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL, 2009.
  • Marco Gaboardi and Romain Péchoux. Upper bounds on stream I/O using semantic interpretations. In CSL 2009, volume 5771, pages 271–286. Springer, 2009.
  • Marco Gaboardi and Romain Péchoux. Global and local space properties of stream programs. In 1st International Workshop on Foundational and Practical Aspects of Resource Analysis – FOPARA’09, volume 6324 of LNCS, pages 51 – 66, 2010.
  • Jean-Yves Marion and Romain Péchoux. Sup-interpretations, a semantic method for static analysis of program resources. ACM Transactions on Computational Logic (TOCL), 10(4):27, 2009.
  • Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Logical semantics for stability. In Samson Abramsky, Michael W. Mislove, and Catuscia Palamidessi, editors, Proceedings of the 25th Conference on Mathematical Foundations of Pro-
  • gramming Semantics (MFPS 2009), volume 249 of Electronic Notes in Theoretical Computer Science, pages 429–449. Elsevier, 2009.
  • Michele Pagani and Simona Ronchi Della Rocca. Linearity, non-determinism and solvability. Fundamenta Informaticae, 103:358–373, 2010.
  • Michele Pagani and Simona Ronchi Della Rocca. Solvability in resource lambda calculus. In Luke Ong, editor, Foundations of Software Science and Computational Structures (FOSSACS 2010), volume 6014 of LNCS, pages 358–373. Springer, 2010.
  • Luca Roversi and Luca Vercelli. Some Complexity and Expressiveness results on Multimodal and Stratified Proof-nets. In Proceedings of TYPES’08, volume 5497 of LNCS, pages 306 – 322. Springer, 2009.

2011:

  • Guillaume Bonfante, Jean-Yves Marion, and Jean-Yves Moyen. Quasi-interpretations a way to control resources. Theoretical Computer Science, 2011.
  • Marco Gaboardi, Luca Paolini, and Mauro Piccolo. Linearity and pcf: a semantic insight! In ICFP 2011 - The 16th ACM SIGPLAN International Conference on Functional Programming, pages 372–384, Tokyo, Japan, September 2011. ACM.
  • Ugo Dal Lago and Marco Gaboardi. Linear dependent types and relative completeness. In LICS, pages 133–142. IEEE Computer Society, 2011.
  • Jean-Yves Marion. A type system for complexity flow analysis. In LICS, pages 123–132. IEEE Computer Society, 2011.
  • Luca Roversi. Linear Lambda Calculus and Deep Inference. In Luke Ong, editor, TLCA 2011 - 10th Typed Lambda Calculi and Applications, Part of RDP’11, volume 6690 of ARCoSS/LNCS, pages 184 – 197. Springer, 2011.

2012:

  • Emanuele Cesena, Marco Pedicini, and Luca Roversi. Typing a Core Binary Field Arithmetic in a Light Logic. In Foundational and Practical Aspects of Resource Analysis, volume 7177 of LNCS, pages 19 – 35. Springer, 2012.
  • Erika De Benedetti and Simona Ronchi Della Rocca. Bounding normalization time through intersection types. In Luca Paolini, editor, Proceedings of ITRS 2012, EPCS, 2012. To appear.
  • Maurizio Dominici, Simona Ronchi Della Rocca, and Paolo Tranquilli. Standardization in resource lambda calculus. In Proceedings of LINEARITY 2012, EPCS, 2012. to appear.
  • Hugo Férée, Emmanuel Hainry, Mathieu Hoyrup, and Romain Péchoux. Characterizing polynomial time complexity of stream programs using interpretations. Submitted to Theoretical Computer Science., 2012.
  • Marco Gaboardi, Jean Yves Marion, and Simona Ronchi Della Rocca. An implicit characterization of pspace. ACM Transactions on Computational Logic, 13(2):18:1–18:36, 2012.
  • Marco Gaboardi and Romain Péchoux. Space analysis of stream programs using interpretations. Submitted to Information & Computation. Under revision, 2012.
  • Marco Gaboardi and Mauro Piccolo. What is a model for a semantically linear λ-calculus? Journal of Logic and Computation, 2012.
  • Jean-Yves Marion and Romain Péchoux. Complexity information flow in a multi-threaded imperative language. CoRR, abs/1203.6878, 2012.
  • Romain P´echoux. Synthesis of sup-interpretations: a survey. Submitted to Theoretical Computer Science. Under revision, 2012.