My main research interests are
- Type Theory
- Programming languages
- Logics
- Semantics
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.
Papers:
[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.