An essence of SSReflect

I. Whiteside, D. Aspinall, G. Grov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

SSReflect is a powerful language for proving theorems in the Coq system. It has been used for some of the largest proofs in formal mathematics thus far. However, although it constructs proofs in a formal system, like most other proof languages the semantics is informal making it difficult to reason about such proof scripts. We give a semantics to a subset of the language, using a hierarchical notion of proof tree, and show some simple transformations on proofs that preserve the semantics.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings
PublisherSpringer-Verlag GmbH
Pages186-201
Number of pages16
ISBN (Electronic)978-3-642-31374-5
ISBN (Print)978-3-642-31373-8
DOIs
Publication statusPublished - 1 Jan 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume7362
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'An essence of SSReflect'. Together they form a unique fingerprint.

Cite this