Barbara Petit

My main research interests are During my thesis, I have worked on calculus with pattern matching, and also on quantum calculus. Now I am working on implicit complexity and theorem provers as a post-doc of the Eternal project.
More precisely, I am trying to define a type system providing complexity bounds for the call-by-value evaluation of functionnal programming languages.
I am also implementing the dlPCF type system with a type inference algorithm. The idea is to automatically get a precise complexity bound for ML programs, with some side conditions to prove using Why3. The correctness of the complexity bounds would be equivalent to these side conditions.


[1] Alejandro Diaz-Caro and Barbara Petit. Linearity in the non-deterministic call-by-value setting. In Wollic, volume 7456 of Lecture Notes in Computer Science, pages 216-231, 2012. [ bib | http ]
[2] Ugo Dal Lago and Barbara Petit. The geometry of types, 2012. Submitted. [ bib | .pdf ]
[3] Ugo Dal Lago and Barbara Petit. Linear dependent types in a call-by-value scenario, 2012. To appear in Principles and Practice of Declarative Programming. [ bib | .pdf ]
[4] Barbara Petit. A polymorphic type system for the lambda-calculus with constructors. In Typed Lambda Calculus and Applications, volume 5608 of Lecture Notes in Computer Science, pages 234-248, 2009. (Best student paper award). [ bib ]
[5] Barbara Petit. Semantics of typed lambda-calculus with constructors. Logical Methods in Computer Science, 7(2), 2011. [ bib | http ]
[6] Barbara Petit. A categorical model for the lambda calculus with constructors. 2012. [ bib | http ]
[7] Barbara Petit. Continuation models for the lambda calculus with constructors, 2012. To appear in Mathematical Foundations of Programming Semantics. [ bib | .html ]

This file was generated by bibtex2html 1.97.