An Essence of SSReflect

Iain Whiteside; David Aspinall; Gudmund Grov

doi:10.1007/978-3-642-31374-5_13

An Essence of SSReflect

Iain Whiteside, David Aspinall, Gudmund Grov

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

2 Citations (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 language	English
Title of host publication	Intelligent Computer Mathematics
Publisher	Springer
Pages	186-201
Number of pages	16
ISBN (Electronic)	978-3-642-31374-5
ISBN (Print)	978-3-642-31373-8
DOIs	https://doi.org/10.1007/978-3-642-31374-5_13
Publication status	Published - 2012
Event	Intelligent 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 2012 → 13 Jul 2012

Publication series

Name	Lecture Notes in Computer Science
Volume	7362
ISSN (Electronic)	0302-9743

Conference

Conference	Intelligent 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
Country/Territory	Germany
City	Bremen
Period	8/07/12 → 13/07/12

Access to Document

10.1007/978-3-642-31374-5_13

Cite this

@inbook{68842351c39c4a9faf8826e3b01c8977,

title = "An Essence of SSReflect",

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. ",

author = "Iain Whiteside and David Aspinall and Gudmund Grov",

year = "2012",

doi = "10.1007/978-3-642-31374-5_13",

language = "English",

isbn = "978-3-642-31373-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "186--201",

booktitle = "Intelligent Computer Mathematics",

note = "Intelligent 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 ; Conference date: 08-07-2012 Through 13-07-2012",

}

Whiteside, I, Aspinall, D & Grov, G 2012, An Essence of SSReflect. in Intelligent Computer Mathematics. Lecture Notes in Computer Science, vol. 7362, Springer, pp. 186-201, Intelligent 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, 8/07/12. https://doi.org/10.1007/978-3-642-31374-5_13

TY - CHAP

T1 - An Essence of SSReflect

AU - Whiteside, Iain

AU - Aspinall, David

AU - Grov, Gudmund

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-31374-5_13

DO - 10.1007/978-3-642-31374-5_13

M3 - Chapter (peer-reviewed)

SN - 978-3-642-31373-8

T3 - Lecture Notes in Computer Science

SP - 186

EP - 201

BT - Intelligent Computer Mathematics

PB - Springer

T2 - Intelligent 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

Y2 - 8 July 2012 through 13 July 2012

ER -

An Essence of SSReflect

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this