Skip navigation
Skip navigation
The system will be down for maintenance between 8:00 and 8:15am on Wednesday 12, December 2018

A mechanisation of some context-free language theory in HOL4

Barthwal, Aditi; Norrish, Michael

Description

We describe the mechanisation of some foundational results in the theory of context-free languages (CFLs), using the HOL4 system. We focus on pushdown automata (PDAs). We show that two standard acceptance criteria for PDAs ("accept-by-empty-stack" and "accept-by-final-state") are equivalent in power. We are then able to show that the pushdown automata (PDAs) and context-free grammars (CFGs) accept the same languages by showing that each can emulate the other. With both of these models to hand,...[Show more]

CollectionsANU Research Publications
Date published: 2014
Type: Journal article
URI: http://hdl.handle.net/1885/68689
Source: Journal of Computer and System Sciences
DOI: 10.1016/j.jcss.2013.05.003

Download

File Description SizeFormat Image
01_Barthwal_A_mechanisation_of_some_2014.pdf269.73 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  27 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator