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

address = "Switzerland",

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

}