Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Pushdown Automata


view this post on Zulip Email Gateway (Oct 17 2025 at 18:55):

From: Peter Lammich <lammich@in.tum.de>
I'm happy to announce the new entry Pushdown Automata, by Kaan Taskin
and Tobias Nipkow.

https://www.isa-afp.org/entries/Pushdown_Automata.html

Abstract

This entry formalizes pushdown automata and proves their equivalence
with context-free grammars. It also shows that acceptance by empty stack
and by final state are equivalent.

--

Peter


Last updated: Oct 20 2025 at 16:27 UTC