Initial commit

25 files changed, 914 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..55388df
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,16 @@
+auto
+_region_.tex
+*.aux
+*.bbl
+*.blg
+*.brf
+*.dvi
+*.fdb_latexmk
+*.fls
+*.fmt
+*.idx
+*.log
+*.lol
+*.out
+*.prv
+*.toc
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..caaeec1
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,10 @@
+all:
+	latexmk -shell-escape -pvc --pdf -interaction=nonstopmode memoria.tex
+
+bare:
+	pdflatex -shell-escape memoria.tex
+
+clean:
+	rm -rf _region_.tex *.aux *.bbl *.blg *.brf *.dvi *.fdb_latexmk *.fls *.fmt *.idx *.log *.lol *.out *.prv *.toc
+
+.PHONY : all clean
diff --git a/bib.bib b/bib.bib
new file mode 100755
index 0000000..aa72a8e
--- /dev/null
+++ b/bib.bib
@@ -0,0 +1,22 @@
+@inproceedings{Gregoire-Leroy-02,
+  author = {Benjamin Gr{\'e}goire and Xavier Leroy},
+  title = {A compiled implementation of strong reduction},
+  booktitle = {International Conference on Functional Programming 2002},
+  pages = {235--246},
+  publisher = {ACM Press},
+  year = 2002,
+  urllocal = {http://gallium.inria.fr/~xleroy/publi/strong-reduction.pdf},
+  urlpublisher = {http://dx.doi.org/10.1145/581478.581501},
+  abstract = {Motivated by applications to proof assistants based on dependent
+types, we develop and prove correct a strong reducer and
+$\beta$-equivalence checker for the $\lambda$-calculus with products,
+sums, and guarded fixpoints.  Our approach is based on compilation to
+the bytecode of an abstract machine performing weak reductions on
+non-closed terms, derived with minimal modifications from the ZAM
+machine used in the Objective Caml bytecode interpreter, and
+complemented by a recursive ``read back'' procedure.  An
+implementation in the Coq proof assistant demonstrates important
+speed-ups compared with the original interpreter-based implementation
+of strong reduction in Coq.},
+  xtopic = {caml}
+}
diff --git a/defs.tex b/defs.tex
new file mode 100755
index 0000000..3cc5e4c
--- /dev/null
+++ b/defs.tex
@@ -0,0 +1,236 @@
+% Source: EasyCrypt manual (https://www.easycrypt.info)
+
+%% Names
+% Tools
+\newcommand{\EasyCrypt}{\textsf{EasyCrypt}\xspace}
+\newcommand{\CertiCrypt}{\textsf{CertiCrypt}\xspace}
+\newcommand{\CertiPriv}{\textsf{CertiPriv}\xspace}
+\newcommand{\SsReflect}{\textsf{SsReflect}\xspace}
+\newcommand{\Coq}{\textsf{Coq}\xspace}
+\newcommand{\WhyThree}{\textsf{Why3}\xspace}
+
+% Languages and Logics
+\newcommand{\pWHILE}{\textsf{p}\textsc{While}\xspace}
+\newcommand{\pRHL}{\textsf{pRHL}\xspace}
+
+%% Security properties and schemes
+\newcommand{\INDCPA}{\textsf{IND-CPA}\xspace}
+\newcommand{\INDCCAone}{\textsf{IND-CCA1}\xspace}
+\newcommand{\INDCCA}{\textsf{IND-CCA}\xspace}
+\newcommand{\EFCMA}{\textsf{EF-CMA}\xspace}
+\newcommand{\LCDH}{\ensuremath{\mathsf{LCDH}}\xspace}
+\newcommand{\CDH}{\textsf{CDH}\xspace}
+\newcommand{\DDH}{\textsf{DDH}\xspace}
+\newcommand{\ElGamal}{\textsf{ElGamal}\xspace}
+\newcommand{\HElGamal}{\textsf{HElGamal}\xspace}
+\newcommand{\RSA}{\textsf{RSA}\xspace}
+\newcommand{\OAEP}{\textsf{OAEP}\xspace}
+\newcommand{\FDH}{\textsf{FDH}\xspace}
+\newcommand{\HMAC}{\textsf{HMAC}\xspace}
+\newcommand{\CS}{\textsf{CS}\xspace}
+\newcommand{\Skein}{\textsf{Skein}\xspace}
+\newcommand{\TCR}{\textsf{TCR}\xspace}
+
+\newcommand{\KG}{\mathcal{KG}}
+\newcommand{\Enc}{\mathcal{E}}
+\newcommand{\Dec}{\mathcal{D}}
+
+%% Complexity and termination
+\newcommand{\lossless}{\mathsf{lossless}}
+
+%% Sets
+\newcommand{\zeroone}{[0,1]}
+\newcommand{\bit}{\{0,1\}}
+\newcommand{\bitstring}[1]{\ensuremath{\bit^{#1}}}
+\newcommand{\bool}{\mathbb{B}}
+\newcommand{\nat}{\mathbb{N}}
+\newcommand{\real}{\mathbb{R}}
+\newcommand{\option}[1]{#1_\bot}
+
+%% Mathematics
+\newcommand{\conv}[1][]{\mathrel{\leftrightarrow^*_{#1}}}
+\renewcommand{\Pr}[2]{\mathrm{Pr}\left[#1 : #2\right]}
+\newcommand{\Prm}[3]{\mathrm{Pr}\left[#1,#3 : #2\right]}
+\newcommand{\labs}{\left\lvert}
+\newcommand{\rabs}{\right\rvert}
+\newcommand{\charfun}{\mathds{1}}
+
+%% Distribution monad
+\newcommand{\supp}{\mathsf{support}}
+\newcommand{\range}[2]{\mathsf{range}~{#1}~{#2}}
+
+%% Semantics
+\newcommand{\subst}[2]{\left[{}^{#2}/{}_{#1}\right]}
+\newcommand{\fv}{\mathsf{fv}}
+\newcommand{\modifies}{\mathsf{mod}}
+\newcommand{\glob}{\mathsf{glob}}
+\newcommand{\Env}{\mathcal{E}}
+
+%% Well-formed adversaries
+%% Program Judgements
+\newcommand{\Hoare}[3]{\left[{#1}:{#2}\Longrightarrow{#3}\right]}
+\newcommand{\Equiv}[4]{\left[{#1}\sim{#2}:{#3}\Longrightarrow{#4}\right]}
+\newcommand{\bdHoareS}[5]{{\Hoare{#1}{#2}{#3}}\,{#4}\,{#5}}
+\newcommand{\HoareLe}[4]{\bdHoareS{#1}{#2}{#3}{\leq}{#4}}
+\newcommand{\HoareEq}[4]{\bdHoareS{#1}{#2}{#3}{=}{#4}}
+\newcommand{\HoareGe}[4]{\bdHoareS{#1}{#2}{#3}{\geq}{#4}}
+
+\newcommand{\side}[1]{\langle #1 \rangle}
+\newcommand{\sidel}{\side{1}}
+\newcommand{\sider}{\side{2}}
+\newcommand{\pre}{\Psi}
+\newcommand{\post}{\Phi}
+\newcommand{\bound}{\delta}
+\newcommand{\ECinsupp}[2]{\mathec{Distr.in_supp}\,{#1}\,{#2}}
+\newcommand{\insupp}[2]{{#1}\in\mathec{supp}\,{#2}}
+
+%% Variables
+\newcommand{\var}[1]{\ensuremath{\mathit{#1}} \xspace}
+
+%% Constants and operators
+\newcommand{\true}{\mathsf{true}}
+\newcommand{\false}{\mathsf{false}}
+\newcommand{\nil}{\mathsf{nil}}
+\newcommand{\hd}{\mathsf{hd}}
+\newcommand{\tl}{\mathsf{tl}}
+\newcommand{\app}{\mathbin{+\mkern-7mu+}}
+\newcommand{\concat}{\parallel}
+\newcommand{\xor}{\oplus}
+\newcommand{\msb}[2]{[#1]^{#2}}
+\newcommand{\lsb}[2]{[#1]_{#2}}
+\newcommand{\dom}{\mathsf{dom}}
+\newcommand{\ran}{\mathsf{ran}}
+\newcommand{\fst}{\mathsf{fst}}
+\newcommand{\snd}{\mathsf{snd}}
+\newcommand{\some}[1]{#1}
+\newcommand{\none}{\bot}
+
+\newcommand{\Int}{\mathsf{Int}}
+\newcommand{\tint}{\mathsf{int}}
+
+\newcommand{\tbool}{\mathsf{bool}}
+
+%% Language
+\newcommand{\Skip}{\mathsf{skip}}
+\newcommand{\Seq}[2]{#1;\ #2}
+\newcommand{\Ass}[2]{#1 \leftarrow #2}
+\newcommand{\Rand}[2]{#1 \stackrel{\raisebox{-.25ex}[.25ex]%
+{\tiny $\mathdollar$}}{\raisebox{-.2ex}[.2ex]{$\leftarrow$}} #2}
+\newcommand{\Randi}[2]{\Rand{#1}{[0..#2]}}
+\newcommand{\Randb}[1]{\Rand{#1}{\bit}}
+\newcommand{\Randbs}[2]{\Rand{#1}{\bitstring{#2}}}
+\newcommand{\Cond}[3]{\mathsf{if}\ #1\ \mathsf{then}\ #2\ \mathsf{else}\ #3}
+\newcommand{\Condt}[2]{\mathsf{if}\ #1\ \mathsf{then}\ #2}
+\newcommand{\Else}{\mathsf{else}\ }
+\newcommand{\Elsif}{\mathsf{elsif}\ }
+\newcommand{\nWhile}[3]{\mathsf{while}_{#1}\ #2\ \mathsf{do}\ #3}
+\newcommand{\While}[2]{\mathsf{while}\ #1\ \mathsf{do}\ #2}
+\newcommand{\Call}[3]{#1 \leftarrow #2\mathsf{(}#3\mathsf{)}}
+\newcommand{\Return}{\mathsf{return}}
+
+%% Language definition
+
+
+\newcounter{easycrypt}
+\lstnewenvironment{easycrypt}[2][]{
+  \renewcommand\lstlistingname{Listado de código}
+  \setcounter{lstlisting}{\value{easycrypt}}
+  \lstset{language=easycrypt,caption={#2},#1}
+}
+{\stepcounter{easycrypt}}
+
+\lstdefinelanguage{easycrypt}{
+  style=easycrypt-default,
+  keywordsprefix={'},
+  morekeywords=[1]{unit,bool,int,real,bitstring,array,list,matrix,word},
+  morekeywords=[2]{type,datatype,op,caxiom,axiom,lemma,module,pred,const,declare},
+  morekeywords=[3]{var,fun,charfun,cost},
+  morekeywords=[4]{while,if},
+  morekeywords=[5]{theory,end,clone,import,export,as,with,section},
+  morekeywords=[6]{forall,exists,lambda},
+  morekeywords=[7]{idtac,change,beta,iota,zeta,logic,delta,simplify,congr,
+    generalize,pose,split,left,right,case,intros,cut,elim,apply,rewrite,elimT,
+    subst,progress,trivial},
+  morekeywords=[8]{by,assumption,smt,reflexivity},
+  morekeywords=[9]{first,last,do,try},
+  morecomment=[n][\itshape]{(*}{*)},
+  morecomment=[n][\bfseries]{(**}{*)}
+}
+
+\lstdefinestyle{easycrypt-default}{
+  columns=fullflexible,
+  % captionpos=b,
+  frame=tb,
+  xleftmargin=.1\textwidth,
+  xrightmargin=.1\textwidth,
+  rangebeginprefix={(**\ begin\ },
+  rangeendprefix={(**\ end\ },
+  rangesuffix={\ *)},
+  includerangemarker=false,
+  basicstyle=\small\sffamily,
+  identifierstyle={},
+  keywordstyle=[1]{\itshape\color{OliveGreen}},
+  keywordstyle=[2]{\bfseries\color{Blue}},
+  keywordstyle=[3]{\bfseries},
+  keywordstyle=[4]{\bfseries},
+  keywordstyle=[5]{\bfseries\color{OliveGreen}},
+  keywordstyle=[6]{\itshape\color{Blue}},
+  keywordstyle=[7]{\color{Blue}},
+  keywordstyle=[8]{\color{Red}},
+  keywordstyle=[9]{\color{OliveGreen}},
+  literate={phi}{{$\!\phi\,$}}1
+           {phi1}{{$\!\phi_1$}}1
+           {phi2}{{$\!\phi_2$}}1
+           {phi3}{{$\!\phi_3$}}1
+           {phin}{{$\!\phi_n$}}1
+}
+
+\newcounter{bnf}
+\lstnewenvironment{bnf}[2][]{
+  \renewcommand\lstlistingname{Gramática}
+  \setcounter{lstlisting}{\value{bnf}}
+  \lstset{language=bnf,caption={#2},#1}
+}
+{\stepcounter{bnf}}
+
+\lstdefinestyle{bnf-style}{
+  frame=tb,
+  keywordstyle=[1]{\bfseries},
+  mathescape=true,
+}
+
+\lstdefinelanguage{bnf}{
+  style=bnf-style,
+  morekeywords=[1]{while,do,if,then,else,skip}
+}
+
+\newcounter{game}
+\lstnewenvironment{game}[2][]{
+  \renewcommand\lstlistingname{Juego}
+  \setcounter{lstlisting}{\value{game}}
+  \lstset{language=game,caption={#2},#1}
+}
+{\stepcounter{game}}
+
+\lstdefinestyle{game-style}{
+  frame=tb,
+  keywordstyle=[1]{\bfseries},
+  mathescape=true,
+}
+
+\lstdefinelanguage{game}{
+  style=game-style,
+}
+
+\newcommand{\rawec}[2][basicstyle=\normalsize\sffamily,mathescape]{\lstinline
+[language=easycrypt,#1]{#2}}
+
+%% Typesetting
+\newcommand{\titledbox}[4]{{\color{#1}\fbox{\begin{minipage}{#2}{\textbf{#3:} \color{black}#4}\end{minipage}}}}
+\newcommand{\warningbox}[1]{\titledbox{red}{.9\textwidth}{Warning}{#1}}
+\newcommand{\futurebox}[1]{\titledbox{blue}{.9\textwidth}{Future}{#1}}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "memoria"
+%%% End:
\ No newline at end of file
diff --git a/img/br93.png b/img/br93.png
new file mode 100644
index 0000000..a6d568a
--- /dev/null
+++ b/img/br93.png
diff --git a/img/browser-post.png b/img/browser-post.png
new file mode 100644
index 0000000..b45eab5
--- /dev/null
+++ b/img/browser-post.png
diff --git a/img/browser-pre.png b/img/browser-pre.png
new file mode 100644
index 0000000..f5849a6
--- /dev/null
+++ b/img/browser-pre.png
diff --git a/img/editor.png b/img/editor.png
new file mode 100644
index 0000000..7bdfa46
--- /dev/null
+++ b/img/editor.png
diff --git a/img/index.png b/img/index.png
new file mode 100644
index 0000000..e47be96
--- /dev/null
+++ b/img/index.png
diff --git a/img/login.png b/img/login.png
new file mode 100644
index 0000000..586d84f
--- /dev/null
+++ b/img/login.png
diff --git a/img/proofs.png b/img/proofs.png
new file mode 100644
index 0000000..381db07
--- /dev/null
+++ b/img/proofs.png
diff --git a/img/register.png b/img/register.png
new file mode 100644
index 0000000..60a41ea
--- /dev/null
+++ b/img/register.png
diff --git a/img/results.png b/img/results.png
new file mode 100644
index 0000000..c28f0d0
--- /dev/null
+++ b/img/results.png
diff --git a/img/web-finished.png b/img/web-finished.png
new file mode 100644
index 0000000..3eb0e5e
--- /dev/null
+++ b/img/web-finished.png
diff --git a/img/web-prototype.png b/img/web-prototype.png
new file mode 100644
index 0000000..f6a5538
--- /dev/null
+++ b/img/web-prototype.png
diff --git a/memoria.pdf b/memoria.pdf
new file mode 100644
index 0000000..62ab0b3
--- /dev/null
+++ b/memoria.pdf
diff --git a/memoria.pyg b/memoria.pyg
new file mode 100644
index 0000000..e46d848
--- /dev/null
+++ b/memoria.pyg
@@ -0,0 +1,95 @@
+
+\makeatletter
+\def\PY@reset{\let\PY@it=\relax \let\PY@bf=\relax%
+    \let\PY@ul=\relax \let\PY@tc=\relax%
+    \let\PY@bc=\relax \let\PY@ff=\relax}
+\def\PY@tok#1{\csname PY@tok@#1\endcsname}
+\def\PY@toks#1+{\ifx\relax#1\empty\else%
+    \PY@tok{#1}\expandafter\PY@toks\fi}
+\def\PY@do#1{\PY@bc{\PY@tc{\PY@ul{%
+    \PY@it{\PY@bf{\PY@ff{#1}}}}}}}
+\def\PY#1#2{\PY@reset\PY@toks#1+\relax+\PY@do{#2}}
+
+\expandafter\def\csname PY@tok@k\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@o\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PY@tok@mf\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PY@tok@gh\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
+\expandafter\def\csname PY@tok@s\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PY@tok@cm\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+\expandafter\def\csname PY@tok@kp\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@nb\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@no\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.53,0.00,0.00}{##1}}}
+\expandafter\def\csname PY@tok@bp\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@nv\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PY@tok@gs\endcsname{\let\PY@bf=\textbf}
+\expandafter\def\csname PY@tok@go\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.53,0.53,0.53}{##1}}}
+\expandafter\def\csname PY@tok@ss\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PY@tok@kr\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@kd\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@mb\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PY@tok@mh\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PY@tok@il\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PY@tok@nn\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
+\expandafter\def\csname PY@tok@kc\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@vg\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PY@tok@err\endcsname{\def\PY@bc##1{\setlength{\fboxsep}{0pt}\fcolorbox[rgb]{1.00,0.00,0.00}{1,1,1}{\strut ##1}}}
+\expandafter\def\csname PY@tok@si\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.73,0.40,0.53}{##1}}}
+\expandafter\def\csname PY@tok@vc\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PY@tok@nd\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
+\expandafter\def\csname PY@tok@gd\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.63,0.00,0.00}{##1}}}
+\expandafter\def\csname PY@tok@m\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PY@tok@c\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+\expandafter\def\csname PY@tok@cs\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+\expandafter\def\csname PY@tok@c1\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.25,0.50,0.50}{##1}}}
+\expandafter\def\csname PY@tok@sb\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PY@tok@sh\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PY@tok@nc\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
+\expandafter\def\csname PY@tok@nf\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,1.00}{##1}}}
+\expandafter\def\csname PY@tok@gi\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.63,0.00}{##1}}}
+\expandafter\def\csname PY@tok@ni\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.60,0.60,0.60}{##1}}}
+\expandafter\def\csname PY@tok@gp\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.00,0.50}{##1}}}
+\expandafter\def\csname PY@tok@kn\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@ge\endcsname{\let\PY@it=\textit}
+\expandafter\def\csname PY@tok@s1\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PY@tok@sx\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@kt\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.69,0.00,0.25}{##1}}}
+\expandafter\def\csname PY@tok@cp\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.74,0.48,0.00}{##1}}}
+\expandafter\def\csname PY@tok@nl\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.63,0.63,0.00}{##1}}}
+\expandafter\def\csname PY@tok@mi\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PY@tok@sd\endcsname{\let\PY@it=\textit\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PY@tok@na\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.49,0.56,0.16}{##1}}}
+\expandafter\def\csname PY@tok@mo\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.40,0.40,0.40}{##1}}}
+\expandafter\def\csname PY@tok@ow\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.67,0.13,1.00}{##1}}}
+\expandafter\def\csname PY@tok@se\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.73,0.40,0.13}{##1}}}
+\expandafter\def\csname PY@tok@w\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.73,0.73}{##1}}}
+\expandafter\def\csname PY@tok@nt\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.00,0.50,0.00}{##1}}}
+\expandafter\def\csname PY@tok@s2\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PY@tok@sc\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.13,0.13}{##1}}}
+\expandafter\def\csname PY@tok@ne\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.82,0.25,0.23}{##1}}}
+\expandafter\def\csname PY@tok@vi\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.10,0.09,0.49}{##1}}}
+\expandafter\def\csname PY@tok@gu\endcsname{\let\PY@bf=\textbf\def\PY@tc##1{\textcolor[rgb]{0.50,0.00,0.50}{##1}}}
+\expandafter\def\csname PY@tok@gt\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.00,0.27,0.87}{##1}}}
+\expandafter\def\csname PY@tok@gr\endcsname{\def\PY@tc##1{\textcolor[rgb]{1.00,0.00,0.00}{##1}}}
+\expandafter\def\csname PY@tok@sr\endcsname{\def\PY@tc##1{\textcolor[rgb]{0.73,0.40,0.53}{##1}}}
+
+\def\PYZbs{\char`\\}
+\def\PYZus{\char`\_}
+\def\PYZob{\char`\{}
+\def\PYZcb{\char`\}}
+\def\PYZca{\char`\^}
+\def\PYZam{\char`\&}
+\def\PYZlt{\char`\<}
+\def\PYZgt{\char`\>}
+\def\PYZsh{\char`\#}
+\def\PYZpc{\char`\%}
+\def\PYZdl{\char`\$}
+\def\PYZhy{\char`\-}
+\def\PYZsq{\char`\'}
+\def\PYZdq{\char`\"}
+\def\PYZti{\char`\~}
+% for compatibility with earlier versions
+\def\PYZat{@}
+\def\PYZlb{[}
+\def\PYZrb{]}
+\makeatother
+
diff --git a/memoria.tex b/memoria.tex
new file mode 100755
index 0000000..3d194e2
--- /dev/null
+++ b/memoria.tex
@@ -0,0 +1,91 @@
+\documentclass[12pt,a4paper,parskip=full]{scrreprt}
+\usepackage[top=3.5cm,bottom=3.5cm,left=3cm,right=3cm]{geometry}
+
+% \usepackage[spanish]{babel}
+\usepackage[utf8]{inputenc} \usepackage{url}
+\usepackage{graphicx} \usepackage{cite} \usepackage{amsmath}
+\usepackage{mathtools} \usepackage{listings} \usepackage{syntax}
+% \usepackage[compact,small]{titlesec}
+\usepackage[usenames,dvipsnames]{xcolor}
+\usepackage[pagebackref,colorlinks=true,linkcolor=black,urlcolor=black,citecolor=blue]{hyperref}
+\usepackage{perpage} \usepackage{subcaption}
+
+\usepackage{tikz}
+% \usepackage{minted}
+
+\usepackage{float}
+\floatstyle{boxed}
+\newfloat{code}{th}{los}[chapter]
+\floatname{code}{Code listing}
+
+\usetikzlibrary{shapes,arrows}
+
+\hypersetup{pageanchor=false}
+
+
+% \input{defs}
+\input{portada/defs}
+
+\MakePerPage{footnote}
+
+\def\emptypage{\newpage\thispagestyle{empty}\mbox{}}
+
+\begin{document}
+\input{portada/portada}
+
+\pagenumbering{roman}
+
+
+\emptypage
+\chapter*{Resumen}
+
+\chapter*{Abstract}
+
+\emptypage
+\tableofcontents
+
+
+\emptypage
+\chapter{INTRODUCTION}
+\label{cha:introduction}
+\pagenumbering{arabic}
+\setcounter{page}{1}
+
+EasyCrypt\footnote{\url{https://www.easycrypt.info/}} is a crypto framework...
+
+
+
+- EasyCrypt
+- Term rewriting
+ - Some theory (books?)
+ - Extensions of lambda calculus
+
+\chapter{STATE OF THE ART}
+
+- Reduction things
+- Abstract machines
+ - Krivine
+ - ZAM\cite{Gregoire-Leroy-02}
+
+\chapter{IMPLEMENTATION}
+
+- Outside EasyCrypt: weak symbolic with fixpts and cases
+
+\chapter{CONTRIBUTIONS}
+\label{cha:contribuciones}
+
+- EasyCrypt rules
+
+\chapter{CONCLUSIONS}
+\label{cha:result-y-concl}
+
+- Writing real things.
+- Hey arst
+
+\chapter{ANNEX}
+\label{cha:anexos}
+
+
+\pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr}
+
+\end{document}
diff --git a/minted.sty b/minted.sty
new file mode 100644
index 0000000..0e0585c
--- /dev/null
+++ b/minted.sty
@@ -0,0 +1,239 @@
+%%
+%% This is file `minted.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% minted.dtx  (with options: `package')
+%% Copyright 2010--2011 Konrad Rudolph
+%% 
+%% This work may be distributed and/or modified under the
+%% conditions of the LaTeX Project Public License, either version 1.3
+%% of this license or (at your option) any later version.
+%% The latest version of this license is in
+%%   http://www.latex-project.org/lppl.txt
+%% and version 1.3 or later is part of all distributions of LaTeX
+%% version 2005/12/01 or later.
+%% 
+%% Additionally, the project may be distributed under the terms of the new BSD
+%% license.
+%% 
+%% This work has the LPPL maintenance status `maintained'.
+%% 
+%% The Current Maintainer of this work is Konrad Rudolph.
+%% 
+%% This work consists of the files minted.dtx and minted.ins
+%% and the derived file minted.sty.
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{minted}[2011/09/17 v1.7 Yet another Pygments shim for LaTeX]
+\RequirePackage{keyval}
+\RequirePackage{fancyvrb}
+\RequirePackage{xcolor}
+\RequirePackage{float}
+\RequirePackage{ifthen}
+\RequirePackage{calc}
+\RequirePackage{ifplatform}
+\DeclareOption{chapter}{\def\minted@float@within{chapter}}
+\DeclareOption{section}{\def\minted@float@within{section}}
+\ProcessOptions\relax
+\ifwindows
+  \providecommand\DeleteFile[1]{\immediate\write18{del #1}}
+\else
+  \providecommand\DeleteFile[1]{\immediate\write18{rm #1}}
+\fi
+\newboolean{AppExists}
+\newcommand\TestAppExists[1]{
+  \ifwindows
+    \DeleteFile{\jobname.aex}
+    \immediate\write18{for \string^\@percentchar i in (#1.exe #1.bat #1.cmd)
+      do set >\jobname.aex <nul: /p x=\string^\@percentchar \string~$PATH:i>>\jobname.aex} %$
+    \newread\@appexistsfile
+    \immediate\openin\@appexistsfile\jobname.aex
+    \expandafter\def\expandafter\@tmp@cr\expandafter{\the\endlinechar}
+    \endlinechar=-1\relax
+    \readline\@appexistsfile to \@apppathifexists
+    \endlinechar=\@tmp@cr
+    \ifthenelse{\equal{\@apppathifexists}{}}
+     {\AppExistsfalse}
+     {\AppExiststrue}
+    \immediate\closein\@appexistsfile
+    \DeleteFile{\jobname.aex}
+\immediate\typeout{file deleted}
+  \else
+    \immediate\write18{which #1 && touch \jobname.aex}
+    \IfFileExists{\jobname.aex}
+     {\AppExiststrue
+      \DeleteFile{\jobname.aex}}
+     {\AppExistsfalse}
+  \fi}
+\newcommand\minted@resetoptions{}
+\newcommand\minted@defopt[1]{
+  \expandafter\def\expandafter\minted@resetoptions\expandafter{%
+    \minted@resetoptions
+    \@namedef{minted@opt@#1}{}}}
+\newcommand\minted@opt[1]{
+  \expandafter\detokenize%
+    \expandafter\expandafter\expandafter{\csname minted@opt@#1\endcsname}}
+\newcommand\minted@define@opt[3][]{
+  \minted@defopt{#2}
+  \ifthenelse{\equal{#1}{}}{
+    \define@key{minted@opt}{#2}{\@namedef{minted@opt@#2}{#3}}}
+   {\define@key{minted@opt}{#2}[#1]{\@namedef{minted@opt@#2}{#3}}}}
+\newcommand\minted@define@switch[3][]{
+  \minted@defopt{#2}
+  \define@booleankey{minted@opt}{#2}
+   {\@namedef{minted@opt@#2}{#3}}
+   {\@namedef{minted@opt@#2}{#1}}}
+\minted@defopt{extra}
+\newcommand\minted@define@extra[1]{
+  \define@key{minted@opt}{#1}{
+    \expandafter\def\expandafter\minted@opt@extra\expandafter{%
+      \minted@opt@extra,#1=##1}}}
+\newcommand\minted@define@extra@switch[1]{
+  \define@booleankey{minted@opt}{#1}
+   {\expandafter\def\expandafter\minted@opt@extra\expandafter{%
+      \minted@opt@extra,#1}}
+   {\expandafter\def\expandafter\minted@opt@extra\expandafter{%
+      \minted@opt@extra,#1=false}}}
+\minted@define@switch{texcl}{-P texcomments}
+\minted@define@switch{mathescape}{-P mathescape}
+\minted@define@switch{linenos}{-P linenos}
+\minted@define@switch{startinline}{-P startinline}
+\minted@define@switch[-P funcnamehighlighting=False]%
+  {funcnamehighlighting}{-P funcnamehighlighting}
+\minted@define@opt{gobble}{-F gobble:n=#1}
+\minted@define@opt{bgcolor}{#1}
+\minted@define@extra{frame}
+\minted@define@extra{framesep}
+\minted@define@extra{framerule}
+\minted@define@extra{rulecolor}
+\minted@define@extra{numbersep}
+\minted@define@extra{firstnumber}
+\minted@define@extra{stepnumber}
+\minted@define@extra{firstline}
+\minted@define@extra{lastline}
+\minted@define@extra{baselinestretch}
+\minted@define@extra{xleftmargin}
+\minted@define@extra{xrightmargin}
+\minted@define@extra{fillcolor}
+\minted@define@extra{tabsize}
+\minted@define@extra{fontfamily}
+\minted@define@extra{fontsize}
+\minted@define@extra{fontshape}
+\minted@define@extra{fontseries}
+\minted@define@extra{formatcom}
+\minted@define@extra{label}
+\minted@define@extra@switch{numberblanklines}
+\minted@define@extra@switch{showspaces}
+\minted@define@extra@switch{resetmargins}
+\minted@define@extra@switch{samepage}
+\minted@define@extra@switch{showtabs}
+\minted@define@extra@switch{obeytabs}
+\newsavebox{\minted@bgbox}
+\newenvironment{minted@colorbg}[1]{
+  \def\minted@bgcol{#1}
+  \noindent
+  \begin{lrbox}{\minted@bgbox}
+  \begin{minipage}{\linewidth-2\fboxsep}}
+ {\end{minipage}
+  \end{lrbox}%
+  \colorbox{\minted@bgcol}{\usebox{\minted@bgbox}}}
+\newwrite\minted@code
+\newcommand\minted@savecode[1]{
+  \immediate\openout\minted@code\jobname.pyg
+  \immediate\write\minted@code{#1}
+  \immediate\closeout\minted@code}
+\newcommand\minted@pygmentize[2][\jobname.pyg]{
+  \def\minted@cmd{pygmentize -l #2 -f latex -F tokenmerge
+    \minted@opt{gobble} \minted@opt{texcl} \minted@opt{mathescape}
+    \minted@opt{startinline} \minted@opt{funcnamehighlighting}
+    \minted@opt{linenos} -P "verboptions=\minted@opt{extra}"
+    -o \jobname.out.pyg #1}
+  \immediate\write18{\minted@cmd}
+  % For debugging, uncomment:
+  %\immediate\typeout{\minted@cmd}
+  \ifthenelse{\equal{\minted@opt@bgcolor}{}}
+   {}
+   {\begin{minted@colorbg}{\minted@opt@bgcolor}}
+  \input{\jobname.out.pyg}
+  \ifthenelse{\equal{\minted@opt@bgcolor}{}}
+   {}
+   {\end{minted@colorbg}}
+  \DeleteFile{\jobname.out.pyg}}
+\newcommand\minted@usedefaultstyle{\usemintedstyle{default}}
+\newcommand\usemintedstyle[1]{
+  \renewcommand\minted@usedefaultstyle{}
+  \immediate\write18{pygmentize -S #1 -f latex > \jobname.pyg}
+  \input{\jobname.pyg}}
+\newcommand\mint[3][]{
+  \DefineShortVerb{#3}
+  \minted@resetoptions
+  \setkeys{minted@opt}{#1}
+  \SaveVerb[aftersave={
+    \UndefineShortVerb{#3}
+    \minted@savecode{\FV@SV@minted@verb}
+    \minted@pygmentize{#2}
+    \DeleteFile{\jobname.pyg}}]{minted@verb}#3}
+\newcommand\minted@proglang[1]{}
+\newenvironment{minted}[2][]
+ {\VerbatimEnvironment
+  \renewcommand{\minted@proglang}[1]{#2}
+  \minted@resetoptions
+  \setkeys{minted@opt}{#1}
+  \begin{VerbatimOut}[codes={\catcode`\^^I=12}]{\jobname.pyg}}%
+ {\end{VerbatimOut}
+  \minted@pygmentize{\minted@proglang{}}
+  \DeleteFile{\jobname.pyg}}
+\newcommand\inputminted[3][]{
+  \minted@resetoptions
+  \setkeys{minted@opt}{#1}
+  \minted@pygmentize[#3]{#2}}
+\newcommand\newminted[3][]{
+  \ifthenelse{\equal{#1}{}}
+   {\def\minted@envname{#2code}}
+   {\def\minted@envname{#1}}
+  \newenvironment{\minted@envname}
+   {\VerbatimEnvironment\begin{minted}[#3]{#2}}
+   {\end{minted}}
+  \newenvironment{\minted@envname *}[1]
+   {\VerbatimEnvironment\begin{minted}[#3,##1]{#2}}
+   {\end{minted}}}
+\newcommand\newmint[3][]{
+  \ifthenelse{\equal{#1}{}}
+   {\def\minted@shortname{#2}}
+   {\def\minted@shortname{#1}}
+  \expandafter\newcommand\csname\minted@shortname\endcsname[2][]{
+    \mint[#3,##1]{#2}##2}}
+\newcommand\newmintedfile[3][]{
+  \ifthenelse{\equal{#1}{}}
+   {\def\minted@shortname{#2file}}
+   {\def\minted@shortname{#1}}
+  \expandafter\newcommand\csname\minted@shortname\endcsname[2][]{
+    \inputminted[#3,##1]{#2}{##2}}}
+\@ifundefined{minted@float@within}
+ {\newfloat{listing}{h}{lol}}
+ {\newfloat{listing}{h}{lol}[\minted@float@within]}
+\newcommand\listingscaption{Listing}
+\floatname{listing}{\listingscaption}
+\newcommand\listoflistingscaption{List of listings}
+\providecommand\listoflistings{\listof{listing}{\listoflistingscaption}}
+\AtBeginDocument{
+  \minted@usedefaultstyle}
+\AtEndOfPackage{
+  \ifnum\pdf@shellescape=1\relax\else
+    \PackageError{minted}
+     {You must invoke LaTeX with the
+      -shell-escape flag}
+     {Pass the -shell-escape flag to LaTeX. Refer to the minted.sty
+      documentation for more information.}\fi
+  \TestAppExists{pygmentize}
+  \ifAppExists\else
+    \PackageError{minted}
+     {You must have `pygmentize' installed
+      to use this package}
+     {Refer to the installation instructions in the minted
+      documentation for more information.}
+  \fi}
+\endinput
+%%
+%% End of file `minted.sty'.
diff --git a/ocaml_colors.tex b/ocaml_colors.tex
new file mode 100644
index 0000000..0f9333c
--- /dev/null
+++ b/ocaml_colors.tex
@@ -0,0 +1,123 @@
+\newcommand\Clinenum[1]{#1}
+\definecolor{CconstructorColor}{rgb}{0.00,0.20,0.80}
+\newcommand\Cconstructor[1]{\textcolor{CconstructorColor}{#1}}
+\definecolor{CcommentColor}{rgb}{0.60,0.00,0.00}
+\newcommand\Ccomment[1]{\textcolor{CcommentColor}{#1}}
+\definecolor{CstringColor}{rgb}{0.67,0.27,0.27}
+\newcommand\Cstring[1]{\textcolor{CstringColor}{#1}}
+\newcommand\Cquotation[1]{#1}
+\definecolor{CalphakeywordColor}{rgb}{0.50,0.50,0.50}
+\newcommand\Calphakeyword[1]{\textcolor{CalphakeywordColor}{#1}}
+\newcommand\Cnonalphakeyword[1]{#1}
+\definecolor{CandColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cand[1]{\textcolor{CandColor}{#1}}
+\definecolor{CasColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cas[1]{\textcolor{CasColor}{#1}}
+\definecolor{CclassColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cclass[1]{\textcolor{CclassColor}{#1}}
+\definecolor{CconstraintColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cconstraint[1]{\textcolor{CconstraintColor}{#1}}
+\definecolor{CexceptionColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cexception[1]{\textcolor{CexceptionColor}{#1}}
+\definecolor{CexternalColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cexternal[1]{\textcolor{CexternalColor}{#1}}
+\definecolor{CfunColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cfun[1]{\textcolor{CfunColor}{#1}}
+\definecolor{CfunctionColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cfunction[1]{\textcolor{CfunctionColor}{#1}}
+\definecolor{CfunctorColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cfunctor[1]{\textcolor{CfunctorColor}{#1}}
+\definecolor{CinColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cin[1]{\textcolor{CinColor}{#1}}
+\definecolor{CinheritColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cinherit[1]{\textcolor{CinheritColor}{#1}}
+\definecolor{CinitializerColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cinitializer[1]{\textcolor{CinitializerColor}{#1}}
+\definecolor{CletColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Clet[1]{\textcolor{CletColor}{#1}}
+\definecolor{CmethodColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cmethod[1]{\textcolor{CmethodColor}{#1}}
+\definecolor{CmoduleColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cmodule[1]{\textcolor{CmoduleColor}{#1}}
+\definecolor{CmutableColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cmutable[1]{\textcolor{CmutableColor}{#1}}
+\definecolor{CofColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cof[1]{\textcolor{CofColor}{#1}}
+\definecolor{CprivateColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cprivate[1]{\textcolor{CprivateColor}{#1}}
+\definecolor{CrecColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Crec[1]{\textcolor{CrecColor}{#1}}
+\definecolor{CtypeColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Ctype[1]{\textcolor{CtypeColor}{#1}}
+\definecolor{CvalColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cval[1]{\textcolor{CvalColor}{#1}}
+\definecolor{CvirtualColor}{rgb}{0.00,0.50,0.00}
+\newcommand\Cvirtual[1]{\textcolor{CvirtualColor}{#1}}
+\definecolor{CdoColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cdo[1]{\textcolor{CdoColor}{#1}}
+\definecolor{CdoneColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cdone[1]{\textcolor{CdoneColor}{#1}}
+\definecolor{CdowntoColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cdownto[1]{\textcolor{CdowntoColor}{#1}}
+\definecolor{CelseColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Celse[1]{\textcolor{CelseColor}{#1}}
+\definecolor{CforColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cfor[1]{\textcolor{CforColor}{#1}}
+\definecolor{CifColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cif[1]{\textcolor{CifColor}{#1}}
+\definecolor{ClazyColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Clazy[1]{\textcolor{ClazyColor}{#1}}
+\definecolor{CmatchColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cmatch[1]{\textcolor{CmatchColor}{#1}}
+\definecolor{CnewColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cnew[1]{\textcolor{CnewColor}{#1}}
+\definecolor{CorColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cor[1]{\textcolor{CorColor}{#1}}
+\definecolor{CthenColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cthen[1]{\textcolor{CthenColor}{#1}}
+\definecolor{CtoColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cto[1]{\textcolor{CtoColor}{#1}}
+\definecolor{CtryColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Ctry[1]{\textcolor{CtryColor}{#1}}
+\definecolor{CwhenColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cwhen[1]{\textcolor{CwhenColor}{#1}}
+\definecolor{CwhileColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cwhile[1]{\textcolor{CwhileColor}{#1}}
+\definecolor{CwithColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cwith[1]{\textcolor{CwithColor}{#1}}
+\definecolor{CassertColor}{rgb}{0.80,0.60,0.00}
+\newcommand\Cassert[1]{\textcolor{CassertColor}{#1}}
+\definecolor{CincludeColor}{rgb}{0.80,0.60,0.00}
+\newcommand\Cinclude[1]{\textcolor{CincludeColor}{#1}}
+\definecolor{CopenColor}{rgb}{0.80,0.60,0.00}
+\newcommand\Copen[1]{\textcolor{CopenColor}{#1}}
+\definecolor{CbeginColor}{rgb}{0.60,0.00,0.60}
+\newcommand\Cbegin[1]{\textcolor{CbeginColor}{#1}}
+\definecolor{CendColor}{rgb}{0.60,0.00,0.60}
+\newcommand\Cend[1]{\textcolor{CendColor}{#1}}
+\definecolor{CobjectColor}{rgb}{0.60,0.00,0.60}
+\newcommand\Cobject[1]{\textcolor{CobjectColor}{#1}}
+\definecolor{CsigColor}{rgb}{0.60,0.00,0.60}
+\newcommand\Csig[1]{\textcolor{CsigColor}{#1}}
+\definecolor{CstructColor}{rgb}{0.60,0.00,0.60}
+\newcommand\Cstruct[1]{\textcolor{CstructColor}{#1}}
+\definecolor{CraiseColor}{rgb}{1.00,0.00,0.00}
+\newcommand\Craise[1]{\textcolor{CraiseColor}{#1}}
+\definecolor{CasrColor}{rgb}{0.50,0.50,0.50}
+\newcommand\Casr[1]{\textcolor{CasrColor}{#1}}
+\definecolor{ClandColor}{rgb}{0.50,0.50,0.50}
+\newcommand\Cland[1]{\textcolor{ClandColor}{#1}}
+\definecolor{ClorColor}{rgb}{0.50,0.50,0.50}
+\newcommand\Clor[1]{\textcolor{ClorColor}{#1}}
+\definecolor{ClslColor}{rgb}{0.50,0.50,0.50}
+\newcommand\Clsl[1]{\textcolor{ClslColor}{#1}}
+\definecolor{ClsrColor}{rgb}{0.50,0.50,0.50}
+\newcommand\Clsr[1]{\textcolor{ClsrColor}{#1}}
+\definecolor{ClxorColor}{rgb}{0.50,0.50,0.50}
+\newcommand\Clxor[1]{\textcolor{ClxorColor}{#1}}
+\definecolor{CmodColor}{rgb}{0.50,0.50,0.50}
+\newcommand\Cmod[1]{\textcolor{CmodColor}{#1}}
+\newcommand\Cfalse[1]{#1}
+\newcommand\Ctrue[1]{#1}
+\definecolor{CbarColor}{rgb}{0.47,0.67,0.67}
+\newcommand\Cbar[1]{\textcolor{CbarColor}{#1}}
diff --git a/portada/defs.tex b/portada/defs.tex
new file mode 100644
index 0000000..30f2888
--- /dev/null
+++ b/portada/defs.tex
@@ -0,0 +1,25 @@
+\usepackage{xcolor}
+
+\usepackage{changepage}
+\usepackage{eso-pic}
+\newcommand\BackgroundPic{
+  \put(-4,0){
+    \parbox[b][\paperheight]{\paperwidth}{
+      \vfill
+      \centering
+      \includegraphics[width=\paperwidth,height=\paperheight]{portada/portada.png}
+      \vfill
+    }
+  }
+}
+
+\definecolor{PortadaBlue}{HTML}{31489F}
+
+\newcommand{\Author}{Guillermo Ramos Gutiérrez}
+\newcommand{\Director}{Manuel Carro Liñares}
+\newcommand{\Codirector}{Pierre-Yves Strub}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../memoria"
+%%% End:
\ No newline at end of file
diff --git a/portada/fic.png b/portada/fic.png
new file mode 100644
index 0000000..2a36204
--- /dev/null
+++ b/portada/fic.png
diff --git a/portada/portada.png b/portada/portada.png
new file mode 100644
index 0000000..c558fa4
--- /dev/null
+++ b/portada/portada.png
diff --git a/portada/portada.tex b/portada/portada.tex
new file mode 100644
index 0000000..a0d532f
--- /dev/null
+++ b/portada/portada.tex
@@ -0,0 +1,57 @@
+\title{\Title}
+\author{\textbf{Autor}: \Author
+  \\\textbf{Director}: \Director}
+
+\AddToShipoutPicture*{\BackgroundPic}
+\newgeometry{inner=1cm,outer=1cm,top=0.5cm,bottom=1cm}
+\begin{titlepage}
+  \begin{figure}
+    \begin{minipage}{.5\linewidth}
+      \begin{flushleft}
+        \includegraphics[scale=0.75]{portada/upmc.png}
+      \end{flushleft}
+    \end{minipage}
+    \begin{minipage}{.5\linewidth}
+      \begin{flushright}
+        \includegraphics[scale=0.185]{portada/fic.png}
+      \end{flushright}
+    \end{minipage}
+  \end{figure}
+
+  \begin{center}
+    {\color{PortadaBlue}
+      { \large \  }\\[0.4cm]
+      { \LARGE \bfseries \underline{Máster Universitario en Software y Sistemas}}\\[1.8cm]
+      { \Large \bfseries Universidad Politécnica de Madrid}\\[0.2cm]
+      { \large Escuela Técnica Superior de Ingenieros Informáticos}\\[2cm]
+      { \LARGE \bfseries TRABAJO FIN DE MÁSTER}\\[3.5cm]
+
+      \begin{adjustwidth}{2cm}{1cm}
+        \begin{center}
+          { \Huge \bfseries {Implementing a term rewriting}}\\[0.5cm]
+          { \Huge \bfseries {engine for the EasyCrypt framework}}\\[2.7cm]
+        \end{center}
+      \end{adjustwidth}
+
+      \begin{adjustwidth}{5.5cm}{1cm}
+        {\Large \textbf{Autor:} \Author }\\[0.3cm]
+        {\Large \textbf{Director:} \Director }\\[0.3cm]
+        {\Large \textbf{Co-director:} \Codirector }\\[2.5cm]
+      \end{adjustwidth}
+
+    }
+  \end{center}
+  \begin{flushright}
+    {\color{PortadaBlue}
+      { \Large  MADRID, JUNIO DE 2014}\\
+    }
+  \end{flushright}
+\end{titlepage}
+
+\ClearShipoutPicture
+\restoregeometry
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../memoria"
+%%% End:
\ No newline at end of file
diff --git a/portada/upmc.png b/portada/upmc.png
new file mode 100644
index 0000000..93ea544
--- /dev/null
+++ b/portada/upmc.png