@inproceedings{Mulligan:2014:LRE:2628136.2628143,
author = {Mulligan, Dominic P. and Owens, Scott and Gray, Kathryn E. and Ridge, Tom and Sewell, Peter},
title = {Lem: Reusable Engineering of Real-world Semantics},
booktitle = {\textbf{ICFP 2014}: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
conf = {ICFP 2014},
year = {2014},
month = sep,
isbn = {978-1-4503-2873-9},
location = {Gothenburg, Sweden},
pages = {175--188},
numpages = {14},
url = {http://doi.acm.org/10.1145/2628136.2628143},
pdf = {http://www.cl.cam.ac.uk/~pes20/lem/built-doc/lem-icfp-2014.pdf},
doi = {10.1145/2628136.2628143},
acmid = {2628143},
publisher = {ACM},
address = {New York, NY, USA},
OPTkeywords = {lem, proof assistants, real-world semantics, specification languages},
abstract ={
Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous semantic models (not just idealised calculi) of real-world processors, programming languages, protocols, and security mechanisms, for testing, proof, analysis, and design. Building these models is challenging, requiring experimentation, dialogue with vendors or standards bodies, and validation; their scale adds engineering issues akin to those of programming to the task of writing clear and usable mathematics. But language and tool support for specification is lacking. Proof assistants can be used but bring their own difficulties, and a model produced in one, perhaps requiring many person-years effort and maintained over an extended period, cannot be used by those familiar with another.
We introduce Lem, a language for engineering reusable large-scale semantic models. The Lem design takes inspiration both from functional programming languages and from proof assistants, and Lem definitions are translatable into OCaml for testing, Coq, HOL4, and Isabelle/HOL for proof, and LaTeX and HTML for presentation. This requires a delicate balance of expressiveness, careful library design, and implementation of transformations - akin to compilation, but subject to the constraint of producing usable and human-readable code for each target. Lem's effectiveness is demonstrated by its use in practice.
}
}
@inproceedings{ITP-sub,
author = {Anthony C. J. Fox},
title = {Improved Tool Support for Machine-Code Decompilation in {HOL4}},
abstract = {The HOL4 interactive theorem prover provides a sound logical environment for reasoning about machine-code programs. The rigour of HOL's LCF-style kernel naturally guarantees very high levels of assurance, but it does present challenges when it comes implementing efficient proof tools. This paper presents improvements that have been made to our methodology for soundly \emph{decompiling} machine-code programs to functions expressed in HOL logic. These advancements have been facilitated by the development of a domain specific language, called L3, for the specification of Instruction Set Architectures (ISAs). As a result of these improvements, decompilation is faster (on average by one to two orders of magnitude), the instruction set specifications are easier to write, and the proof tools are easier to maintain.
},
booktitle = {{\textbf{ITP 2015}}:Interactive Theorem Proving - 6th International Conference, Nanjing, China},
conf = {ITP 2015},
pages = {187--202},
year = {2015},
month = aug,
OPTcrossref = {DBLP:conf/itp/2015},
url = {http://dx.doi.org/10.1007/978-3-319-22102-1_12},
pdf = {http://www.cl.cam.ac.uk/~acjf3/papers/itp15.pdf},
doi = {10.1007/978-3-319-22102-1_12},
timestamp = {Mon, 24 Aug 2015 16:29:06 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/itp/Fox15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@Misc{BasileMPRI,
OPTkey = {},
author = {Basile Clement},
title = {Running programming language specifications},
OPThowpublished = {},
month = aug,
year = 2014,
note = {MPRI report},
conf = {MPRI report},
OPTannote = {}
}
@InProceedings{PittsAM:deptta,
author = {A. M. Pitts and J. Matthiesen and J. Derikx},
title = {A Dependent Type Theory with Abstractable Names},
booktitle = {\textbf{LSFA 2014}: Proceedings of the 9th Workshop on Logical and
Semantic Frameworks, with Applications},
conf = {LSFA 2014},
year = 2015,
month = apr,
editor = {I. Mackie and M. Ayala-Rincon},
volume = 312,
series = {Electronic Notes in Theoretical Computer Science},
pages = {19--50},
doi = {http://dx.doi.org/10.1016/j.entcs.2015.04.003},
pdf = {https://www.repository.cam.ac.uk/bitstream/handle/1810/247863/Pitts_et_al-2015-Electronic_Notes_in_Theoretical_Computer_Science.pdf?sequence=1},
abstract = {This paper describes a version of Martin-Löf's dependent type theory extended with names and constructs for freshness and name-abstraction derived from the theory of nominal sets. We aim for a type theory for computing and proving (via a Curry-Howard correspondence) with syntactic structures which captures familiar, but informal, "nameful" practices when dealing with binders.},
publisher = {Elsevier}
}