Aditi Barthwal
I am a PhD student under Dr. Michael Norrish in the Computer Sciences Laboratory at the Australian National University.
I am interested in automated reasoning.
Publications
 Aditi Barthwal and Michael Norrish,
A Formalisation of the Normal Forms of ContextFree Grammars, Proceedings of CSL, Brno, 2010. LNCS 6247, pp95109.
 Aditi Barthwal and Michael Norrish,
Mechanisation of PDA and Grammar Equivalence for ContextFree Languages, Proceedings of WoLLIC, Brasilia, 2010. LNCS 6188, pp125135.
 Aditi Barthwal and Michael Norrish,
Verified, Executable Parsing, Proceedings of ESOP, York, 2009. LNCS 5502, pp160174.
 Malcolm Newey, Aditi Barthwal and Michael Norrish,
Optimizing Proof for Replay, TPHOLs 2005.
Mechanisation in HOL4
 Verified contextfreegrammars(CFG) (using sets), source code
 Verified, executable SLR parser, source code
 Theory of contextfree grammars and PDA (using lists), source code
 Pumping lemma for contextfree grammars, source code
 Normal Forms for CFGs (using lists), source code
Some past presentations

Formalising the Normal Forms of CFGs in HOL4 (modified version), Technische Universitaet Muenchen (TUM) 2010 Slides

Formalising the Normal Forms of CFGs in HOL4, CSL 2010 Slides

A Formalisation of the Equivalence of CFGs and PDA in HOL4, WoLLIC 2010, Slides

Verified, Executable Parsing, ESOP 2009, Slides

Verified, Executable Parsing (extended version), Cambridge Automated Reasoning Group 2009, Slides
Email to: aditi.barthwal@rsise.anu.edu.au