-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.tex
160 lines (123 loc) · 4.73 KB
/
main.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
\documentclass[bsc,frontabs,twoside,singlespacing,parskip,deptreport]{infthesis}
% \usepackage{amsmath,amstext,amsthm,amssymb}
% \usepackage{agda}
% \usepackage{upgreek}
% \usepackage{balance}
% \usepackage[english]{babel}
% \usepackage{hyperref,cleveref}
% \usepackage{catchfilebetweentags}
\usepackage{agda}
% The following packages are needed because unicode
% is translated (using the next set of packages) to
% latex commands. You may need more packages if you
% use more unicode characters:
\usepackage{textgreek}
\usepackage{amssymb}
\usepackage{bbm}
\usepackage[greek,english]{babel}
\usepackage{amsthm}
\usepackage{catchfilebetweentags}
\usepackage{mathrsfs}
% This handles the translation of unicode to latex:
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{autofe}
% Some characters that are not automatically defined
% (you figure out by the latex compilation errors you get),
% and you need to define:
\DeclareUnicodeCharacter{8988}{\ensuremath{\ulcorner}}
\DeclareUnicodeCharacter{8989}{\ensuremath{\urcorner}}
\DeclareUnicodeCharacter{8803}{\ensuremath{\overline{\equiv}}}
\DeclareUnicodeCharacter{0411}{\ensuremath{\lambda}}
\DeclareUnicodeCharacter{8718}{\ensuremath{\square}}
\DeclareUnicodeCharacter{8759}{::}
\DeclareUnicodeCharacter{10218}{\ensuremath{\langle\langle}}
\DeclareUnicodeCharacter{10219}{\ensuremath{\rangle\rangle}}
\DeclareUnicodeCharacter{120038}{\ensuremath{\mathcal{W}}}
\DeclareUnicodeCharacter{7473}{\textsuperscript{E}}
% Add more as you need them (shouldn't happen often).
\theoremstyle{definition}
\newtheorem*{definition}{Definition}
\begin{document}
\title{Type-preserving closure conversion of PCF in Agda (more to come)}
\author{Piotr Jander}
\course{Master of Informatics}
\project{{\bf MInf Project (Part 2) Report}}
\date{\today}
\abstract{
This is an example of {\tt infthesis} style.
The file {\tt skeleton.tex} generates this document and can be
used to get a ``skeleton'' for your thesis.
The abstract should summarise your report and fit in the space on the
first page.
%
You may, of course, use any other software to write your report,
as long as you follow the same style. That means: producing a title
page as given here, and including a table of contents and bibliography.
}
\maketitle
\section*{Acknowledgements}
Acknowledgements go here.
\tableofcontents
%\pagenumbering{arabic}
\chapter{Introduction}
The document structure should include:
\begin{itemize}
\item
The title page in the format used above.
\item
An optional acknowledgements page.
\item
The table of contents.
\item
The report text divided into chapters as appropriate.
\item
The bibliography.
\end{itemize}
Commands for generating the title page appear in the skeleton file and
are self explanatory.
The file also includes commands to choose your report type (project
report, thesis or dissertation) and degree.
These will be placed in the appropriate place in the title page.
The default behaviour of the documentclass is to produce documents typeset in
12 point. Regardless of the formatting system you use,
it is recommended that you submit your thesis printed (or copied)
double sided.
The report should be printed single-spaced.
It should be 30 to 60 pages long, and preferably no shorter than 20 pages.
Appendices are in addition to this and you should place detail
here which may be too much or not strictly necessary when reading the relevant section.
\section{Using Sections}
Divide your chapters into sub-parts as appropriate.
\section{Citations}
Note that citations
(like \cite{P1} or \cite{P2})
can be generated using {\tt BibTeX} or by using the
{\tt thebibliography} environment. This makes sure that the
table of contents includes an entry for the bibliography.
Of course you may use any other method as well.
\section{Options}
There are various documentclass options, see the documentation. Here we are
using an option ({\tt bsc} or {\tt minf}) to choose the degree type, plus:
\begin{itemize}
\item {\tt frontabs} (recommended) to put the abstract on the front page;
\item {\tt twoside} (recommended) to format for two-sided printing, with
each chapter starting on a right-hand page;
\item {\tt singlespacing} (required) for single-spaced formating; and
\item {\tt parskip} (a matter of taste) which alters the paragraph formatting so that
paragraphs are separated by a vertical space, and there is no
indentation at the start of each paragraph.
\end{itemize}
\chapter{The Real Thing}
% \include{PCF}
% \include{Closure}
% \include{Conversion}
% \include{SubContext}
\include{StateOfTheArt/Bisimulation}
Of course
you may want to use several chapters and much more text than here.
% use the following and \cite{} as above if you use BibTeX
% otherwise generate bibtem entries
\bibliographystyle{plain}
\bibliography{mybibfile}
\end{document}