An Essence of SSReflect

Iain Whiteside, David Aspinall, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

1 Citation (Scopus)

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
PublisherSpringer
Pages186-201
Number of pages16
ISBN (Electronic)978-3-642-31374-5
ISBN (Print)978-3-642-31373-8
DOIs
Publication statusPublished - 2012
EventIntelligent Computer Mathematics 11th 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
Duration: 8 Jul 201213 Jul 2012

Publication series

NameLecture Notes in Computer Science
Volume7362
ISSN (Electronic)0302-9743

Conference

ConferenceIntelligent Computer Mathematics 11th 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
CountryGermany
CityBremen
Period8/07/1213/07/12

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

Cite this