Task 1 Papers
[1] 
Anthony C. J. Fox.
Improved tool support for machinecode decompilation in HOL4.
In ITP 2015:Interactive Theorem Proving  6th
International Conference, Nanjing, China, pages 187202, August 2015.
[ bib 
DOI 
http 
.pdf ]
The HOL4 interactive theorem prover provides a sound logical environment for reasoning about machinecode programs. The rigour of HOL's LCFstyle 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 decompiling machinecode 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.

[2] 
A. M. Pitts, J. Matthiesen, and J. Derikx.
A dependent type theory with abstractable names.
In I. Mackie and M. AyalaRincon, editors, LSFA 2014:
Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with
Applications, volume 312 of Electronic Notes in Theoretical Computer
Science, pages 1950. Elsevier, April 2015.
[ bib 
DOI 
http ]
This paper describes a version of MartinLöf's dependent type theory extended with names and constructs for freshness and nameabstraction derived from the theory of nominal sets. We aim for a type theory for computing and proving (via a CurryHoward correspondence) with syntactic structures which captures familiar, but informal, "nameful" practices when dealing with binders.

[3] 
Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell.
Lem: Reusable engineering of realworld semantics.
In ICFP 2014: Proceedings of the 19th ACM SIGPLAN
International Conference on Functional Programming, pages 175188, New
York, NY, USA, September 2014. ACM.
[ bib 
DOI 
http 
.pdf ]
Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous semantic models (not just idealised calculi) of realworld 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 personyears effort and maintained over an extended period, cannot be used by those familiar with another.

[4]  Basile Clement. Running programming language specifications, August 2014. MPRI report. [ bib ] 
This file was generated by bibtex2html 1.96.