[Club2] Aditi Barthwal on Chomsky & Greibach NF

[Jasmin Blanchette]

Hi all,

Aditi Barthwal will be visiting us from August 17 to August 20 on her way to Cambridge. She's a Ph.D. student of Michael Norrish. I've tentatively scheduled a 45-minute talk on Thursday August 19 at 14:00 in Turing (00.09.055) -- I'll send a reminder.


Topic: Context-Free Language Normalisation Formalisation

Abstract:

As part of a bigger project, we have formalised the theory of context-free languages using HOL4.  Among other results, we have verified the normalisation of context-free grammars  to Chomsky Normal Form and Greibach Normal Form. In this talk, I will present the formalisation of the process to convert a  CFG to GNF in light of the issues that become the central theme when porting a pen and paper proof to a theorem prover such as HOL4. The top level statements look (almost) exactly like the textbook statements but what goes behind the scenes during mechanisation involves strategies far beyond the text treatment. This essentially leads to a "reproving"  of the proof in a theorem prover.

Autobio:

I’m a PhD student at The Australian National University, Canberra under Michael Norrish. My PhD project involves verifying a large chunk of context-free language theory using HOL4. The work is primarily based on Introduction to Automata Theory, Languages and Computation by Hopcroft and Ullman, a standard text for teaching Automata and Language theory. My research interest is in theorem proving and how to make it accessible to a wider audience. I also dabble in anything else that catches my fancy.


Hope to see you there!

Jasmin