Aditi Barthwal

I am a PhD student under Dr. Michael Norrish in the Computer Sciences Laboratory at the Australian National University.

Publications

1. Aditi Barthwal and Michael Norrish, A Formalisation of the Normal Forms of Context-Free Grammars, Proceedings of CSL, Brno, 2010. LNCS 6247, pp95-109.
2. Aditi Barthwal and Michael Norrish, Mechanisation of PDA and Grammar Equivalence for Context-Free Languages, Proceedings of WoLLIC, Brasilia, 2010. LNCS 6188, pp125-135.
3. Aditi Barthwal and Michael Norrish, Verified, Executable Parsing, Proceedings of ESOP, York, 2009. LNCS 5502, pp160-174.
4. Malcolm Newey, Aditi Barthwal and Michael Norrish, Optimizing Proof for Replay, TPHOLs 2005.

Mechanisation in HOL4

• Verified context-free-grammars(CFG) (using sets), source code
• Verified, executable SLR parser, source code
• Theory of context-free grammars and PDA (using lists), source code
• Pumping lemma for context-free 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

Resume