Lisa Allali Ph.D. student - Team Typical (ex-Logical) under the direction of Gilles Dowek Office 00-1028 [my firstname].[my lastname]@gmail.com

Interests

• Proof theory
  
• Deduction modulo
  
• Super-consistency
  
• Supernatural deduction
  
• Rewriting
  
• Types theory
  
• Calculus of inductive constructions
  
• The proof assistant Coq
  

Papers

• Cut elimination in classical sequent calculus modulo a super-consistent theory (written with Olivier Hermant)
• Inductives Types as Equation (written with Paul Brauner) - draft
• A semantic normalization proof for system T (written with Paul Brauner), long version
• Algorithmic equality in Heyting Arithmetic modulo TYPES 2007 proceedings
• Algorithmic equality in Heyting Arithmetic modulo (short version) - HOR 2007 proceedings
• A modulo conservative extension of Heyting Arithmetic - master thesis report (in french) 2006

Presentations

• June 2008 : Lecture at the Typical seminar - Deduction modulo et coupures (in french)
  
• May 2007 : Lecture at TYPES - slides
  
• September 2006 : Master 2 presentation - slides
  
• April 2006 : Seminar deduction modulo (lri - logical - loria ...) - presentation of a paper on arithmetique in deduction modulo - slides
  
• September 2005 : Barcelona - slides
  
• March 2005 : Presentation of the Phd thesis of Julien Allali : Modelisation and comparison on RNA secondary structure  - slides
  
• September 2004 : Lille - slides
  

Teaching

• 2006-2009 : Monitorat at the muséum d'histoire naturelle
        Support for the introduction to HTML course
        Support for the introduction to LATEX course
  
  
• 2003-2004 : TP of LISP and Introduction to computer science to 1st-year students of MIASS at the Computer Science department of Paris 8 university

Interships in laboratories

•  2006  - march/august -  Palaiseau   ( Coq ) 
  Equality in arithmetic deduction modulo
  Team Logical - Department of computer science of the école Polytechnique
  Under the direction of Gilles Dowek
  
  
•  2005  - june/august -  Barcelona ( C ) 
  Study and implementation of placement optimisation algorithms
  Team Gavina - Group on Algorithms for VLSI Design Automation - Department LSI of l'Université Polytechnique of Catalugna
  Under the direction of Jordi Cortadella
  
  
• 2005 - may -   Paris ( Caml )
  Implementation of accessibility algorithms on  processi rewrite systems of tree automata  (with the help of Timbuk )
  Team Liafa - Univertity of Paris 7 Jussieu
  Under the direction of Mihaela Sighireanu and Tayssir Touili
  
  
• 2004 - june/august -  Lille ( JAVA )
  SiMule - Reactifs multi-agents systems on wide scale
  Team SMAC - Lifl
  Under the direction of Philippe Mathieu et Sébastien Picault
  

School

• 2004-2006 : Parisian Master of Research in Computer Science (MPRI)
  
• 2003-2006 : Magister STIC at the Ecole Normale Supérieure of Cachan
  
• 2001-2003 : DEUG Miass at the Paris 8 University