source: Papers/jar-assembler-2014/boender-jar-2014.tex @ 3514

Last change on this file since 3514 was 3514, checked in by mulligan, 5 years ago

added outline of new paper

File size: 4.1 KB
Line 
1\documentclass[a4paper]{article}
2\usepackage{algpseudocode}
3\usepackage{alltt}
4\usepackage{amsfonts}
5\usepackage{amsmath}
6\usepackage[british]{babel}
7\usepackage{caption}
8\usepackage[colorlinks]{hyperref}
9\usepackage[utf8]{inputenc}
10\usepackage{listings}
11\usepackage{microtype}
12\usepackage{subcaption}
13
14\usepackage{kpfonts}
15\usepackage[T1]{fontenc}
16
17\bibliographystyle{alpha}
18
19\renewcommand{\verb}{\lstinline}
20\def\lstlanguagefiles{lst-grafite.tex}
21\lstset{language=Grafite}
22
23\author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen}
24\title{On the proof of correctness of a verified optimising assembler
25\thanks{Research supported by the CerCo project, within the Future and Emerging Technologies (FET) programme of the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number 243881}}
26\date{\today}
27
28\begin{document}
29
30\maketitle
31
32\begin{abstract}
33\end{abstract}
34
35\newpage
36
37\tableofcontents
38
39\newpage
40
41%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
42% Section                                 %
43%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
44\section{Introduction}
45\label{sect.introduction}
46
47% Everybody
48
49%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
50% Section                                 %
51%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
52\subsection{Matita}
53\label{subsect.matita}
54
55% CSC
56
57%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
58% Section                                 %
59%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
60\subsection{Map of paper}
61\label{subsect.map.of.paper}
62
63% Anybody
64
65%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
66% Section                                 %
67%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
68\section{The proof}
69\label{sect.the.proof}
70
71%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
72% Section                                 %
73%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
74\subsection{Structure of the assembler}
75\label{subsect.structure.of.the.assembler}
76
77% Everybody
78
79%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
80% Section                                 %
81%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
82\subsection{Encoding the instruction set}
83\label{subsect.encoding.the.instruction.set}
84
85% DPM and CSC
86
87% Polymorphic variants
88% Non-regularity of instruction set (CISC)
89% Use of dependent types in get_arg_XXX and set_arg_XXX
90% Assembly code features (what pseudo-instructions are present)
91
92%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
93% Section                                 %
94%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
95\subsection{Operational semantics}
96\label{subsect.operational.semantics}
97
98% DPM and CSC
99
100% Trie data structure and use of dependent types
101% Operational semantics of MCS-51
102% Operational semantics of assembly code
103
104%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
105% Section                                 %
106%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
107\subsection{Policies and the correctness proof}
108\label{subsect.policies.and.the.correctness.proof}
109
110% DPM and CSC
111
112%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
113% Section                                 %
114%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
115\subsection{Correctness of branch displacement}
116\label{subsect.correctness.of.branch.displacement}
117
118% JB and CSC
119
120%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
121% Section                                 %
122%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
123\subsection{Fitting together}
124\label{subsect.fitting.together}
125
126% Everybody
127
128%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
129% Section                                 %
130%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
131\section{Conclusion}
132\label{sect.conclusion}
133
134% Everbody
135
136%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
137% Section                                 %
138%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
139\subsection{Related work}
140\label{subsect.related.work}
141
142% Everybody
143
144%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
145% Section                                 %
146%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
147\subsection{Formalisation}
148\label{subsect.formalisation}
149
150% Everybody
151
152% Man-hours of effort
153% Lines of code, etc.
154% Pointer to web address for formalisation
155
156\newpage
157
158\bibliography{boender-jar-2014}
159
160\end{document}
Note: See TracBrowser for help on using the repository browser.