71 lines
3.6 KiB
Org Mode
71 lines
3.6 KiB
Org Mode
|
* TODO Scaletta [1/2]
|
||
|
|
- [X] Abstract
|
||
|
|
- [ ] Introduction [0%]
|
||
|
|
- [ ] Ocaml
|
||
|
|
- [ ] Pattern matching
|
||
|
|
- [ ] Translation Verification
|
||
|
|
- [ ] Symbolic execution
|
||
|
|
|
||
|
|
#+TITLE: Translation Verification of the OCaml pattern matching compiler
|
||
|
|
#+AUTHOR: Francesco Mecca
|
||
|
|
#+EMAIL: me@francescomecca.eu
|
||
|
|
#+DATE:
|
||
|
|
|
||
|
|
#+LANGUAGE: en
|
||
|
|
#+LaTeX_CLASS: article
|
||
|
|
#+LaTeX_HEADER: \usepackage[utf8]{inputenc}
|
||
|
|
#+LaTeX_HEADER: \usepackage{algorithm}
|
||
|
|
#+LaTeX_HEADER: \usepackage{algpseudocode}
|
||
|
|
#+LaTeX_HEADER: \usepackage{amsmath,amssymb,amsthm}
|
||
|
|
#+Latex_HEADER: \newtheorem{definition}{Definition}
|
||
|
|
#+LaTeX_HEADER: \usepackage{graphicx}
|
||
|
|
#+LaTeX_HEADER: \usepackage{listings}
|
||
|
|
#+LaTeX_HEADER: \usepackage{color}
|
||
|
|
#+EXPORT_SELECT_TAGS: export
|
||
|
|
#+EXPORT_EXCLUDE_TAGS: noexport
|
||
|
|
#+OPTIONS: H:2 toc:nil \n:nil @:t ::t |:t ^:{} _:{} *:t TeX:t LaTeX:t
|
||
|
|
#+STARTUP: showall
|
||
|
|
\begin{abstract}
|
||
|
|
|
||
|
|
This dissertation presents an algorithm for the translation validation of the OCaml
|
||
|
|
pattern matching compiler. Given the source representation of the target program and the
|
||
|
|
target program compiled in untyped lambda form, the algoritmhm is capable of modelling
|
||
|
|
the source program in terms of symbolic constraints on it's branches and apply symbolic
|
||
|
|
execution on the untyped lambda representation in order to validate wheter the compilation
|
||
|
|
produced a valid result.
|
||
|
|
In this context a valid result means that for every input in the domain of the source
|
||
|
|
program the untyped lambda translation produces the same output as the source program.
|
||
|
|
The input of the program is modelled in terms of symbolic constraints closely related to
|
||
|
|
the runtime representation of OCaml objects and the output consists of OCaml code
|
||
|
|
blackboxes that are not evaluated in the context of the verification.
|
||
|
|
|
||
|
|
\end{abstract}
|
||
|
|
|
||
|
|
* Introduction
|
||
|
|
|
||
|
|
** TODO OCaml
|
||
|
|
Objective Caml (OCaml) is a dialect of the ML (Meta-Language) family of programming
|
||
|
|
languages.
|
||
|
|
OCaml shares many features with other dialects of ML, such as SML and Caml Light,
|
||
|
|
The main features of ML languages are the use of the Hindley-Milner type system that
|
||
|
|
provides with respect to static type systems of traditional imperative and/or object
|
||
|
|
oriented language such as C, C++ and Java many advantages such as:
|
||
|
|
- Parametric polymorphism: in certain scenarios a function can accept more than one
|
||
|
|
type for the input parameters. For example a function that computes the lenght of a
|
||
|
|
list doesn't need to inspect the type of the elements of the list and for this reason
|
||
|
|
a List.length function can accept list of integers, list of strings and in general
|
||
|
|
list of any type. Such languages offer polymorphic functions through subtyping at
|
||
|
|
runtime only, while other languages such as C++ offer polymorphism through compile
|
||
|
|
time templates and function overloading.
|
||
|
|
With the Hindley-Milner type system each well typed function can have more than one
|
||
|
|
type but always has a unique best type, called the /principal type/.
|
||
|
|
For example the principal type of the List.length function is "For any /a/, function from
|
||
|
|
list of /a/ to /int/" and /a/ is called the /type parameter/.
|
||
|
|
- Strong typing: Languages such as C and C++ allow the programmer to operate on data
|
||
|
|
without considering its type, mainly through pointers. Other languages such as C#
|
||
|
|
and Go allow type erasure so at runtime the type of the data can't be queried.
|
||
|
|
In the case of programming languages using an Hindley-Milner type system the
|
||
|
|
programmer is not allowed to operate on data by ignoring or promoting its type.
|
||
|
|
- Type Inference: the principal type of a well formed term can be inferred without any
|
||
|
|
annotation or declaration.
|