Students' Proof Assistant (SPA)

The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a miniature proof assistant inside the Isabelle proof assistant. In addition we conjecture that a good way to teach stru...

Full description

Bibliographic Details
Main Authors: Anders Schlichtkrull, Jørgen Villadsen, Andreas Halkjær From
Format: Article
Language:English
Published: Open Publishing Association 2019-04-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1904.00617v1