@inproceedings{b4a6f9c6b0e54035bcaa0eae7bf6f1a6,

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 = "I. Whiteside and D. Aspinall and G. Grov",

year = "2012",

month = jan,

day = "1",

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

pages = "186--201",

booktitle = "Intelligent Computer Mathematics",

}