-
Notifications
You must be signed in to change notification settings - Fork 0
/
thesis.lhs
151 lines (116 loc) · 3.38 KB
/
thesis.lhs
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
\documentclass[11pt,a4paper,headings]{scrbook}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[english]{babel}
\usepackage{csquotes}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{setspace}
\usepackage[top=3cm,bottom=3cm,inner=3cm,outer=2cm]{geometry}
\usepackage[Lenny]{fncychap}
\usepackage[headsepline]{scrlayer-scrpage}
\usepackage{bussproofs}
\usepackage{tikz}
\usepackage{tikz-qtree}
\usepackage{tabularx}
\usepackage{ltablex}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{hyperref}
\usepackage{cleveref}
\usepackage[backend=biber]{biblatex}
\usepackage{listings}
%include format.fmt
%include commands.lhs
%Configuration:
\allowdisplaybreaks[1]
\newtheorem{definition}{Definition}
\hypersetup{
pdftitle = {Implementating an Operational Semantics and
Nondeterminism Analysis for a Functional-Logic Language},
pdfauthor = {Fabian Zaiser},
pdfkeywords = {CuMin,
Curry,
SaLT,
Functional-Logic Programming,
nondeterminism,
operational semantics},
}
\bibliography{thesis}
\begin{document}
\frontmatter
\begin{titlepage}
\begin{center}
\textsc{\Large Rheinische Friedrich-Wilhelms-Universität Bonn} \\
\vfill
\textsc{\LARGE Bachelor Thesis}\\
\vfill
\rule{\linewidth}{1pt}
\begin{spacing}{1.2}
\Huge
Implementing an Operational Semantics and Nondeterminism Analysis
for a Functional-Logic Language \\[-0.3cm]
\end{spacing}
\rule{\linewidth}{1pt}
\vfill
\begin{spacing}{1.2}
\LARGE
\textbf{Fabian Moritz Frank Zaiser} \\
Student number: XXXXXX \\
STREET NUMBER \\
D-53121 Bonn
\end{spacing}
\vfill
\textit{\Large \today} \\
\vfill
{\Large
Supervisor: Jun.-Prof.\ Dr.\ rer.\ nat.\ habil.\ Janis Voigtländer
} \\
\vfill
\begin{spacing}{1.2}
\Large
Institute for Computer Science, Department III \\
Römerstraße 164 \\
D-53117 Bonn
\end{spacing}
\end{center}
\end{titlepage}
\chapter*{Eigenständigkeitserklärung}
Hiermit erkläre ich, Fabian Moritz Frank Zaiser,
dass ich die vorliegende Bachelorarbeit selbstständig verfasst
und keine anderen als die angegebenen Quellen und Hilfsmittel benutzt,
sowie Zitate kenntlich gemacht habe.
\vspace{3cm}
\begin{tabular}{lp{2em}l}
\hspace{3cm} && \hspace{6cm} \\ \hline
Ort, Datum && Unterschrift \\
\end{tabular}
\cleardoublepage
\chapter*{Abstract}
Functional-logic languages like Curry aim
to combine the strengths of both functional and logic languages.
In order to establish free theorems for such languages,
the authors of \cite{orig} have focused their attention
on a sublanguage they call \emph{\cumin{}},
which can be translated to another language called \emph{\salt{}}
where logic features like nondeterminism are more explicit.
In this thesis, I will give a detailed exposition of the two languages.
Moreover, I will document
the implementation of an operational semantics for \cumin{}
and of a translation algorithm
that transforms \cumin{} programs into equivalent \salt{} programs.
I will describe how the generated \salt{} code can be simplified
and how it can be used to analyze
the nondeterminism in the original \cumin{} program.
\tableofcontents
\mainmatter
%include 1-introduction.lhs
%include 2-preliminaries.lhs
%include 3-operational.lhs
%include 4-translation.lhs
%include 5-analysis.lhs
%include 6-conclusion.lhs
\printbibliography
\end{document}