From 3d916d10b90ce767b562cc7812a59acbd90a64af Mon Sep 17 00:00:00 2001 From: Guillermo Ramos Date: Thu, 25 Jun 2015 03:43:27 +0200 Subject: Initial commit --- .gitignore | 16 ++++ Makefile | 10 +++ bib.bib | 22 +++++ defs.tex | 236 +++++++++++++++++++++++++++++++++++++++++++++++++ img/br93.png | Bin 0 -> 159393 bytes img/browser-post.png | Bin 0 -> 32568 bytes img/browser-pre.png | Bin 0 -> 27742 bytes img/editor.png | Bin 0 -> 68100 bytes img/index.png | Bin 0 -> 84982 bytes img/login.png | Bin 0 -> 80835 bytes img/proofs.png | Bin 0 -> 65040 bytes img/register.png | Bin 0 -> 84886 bytes img/results.png | Bin 0 -> 44197 bytes img/web-finished.png | Bin 0 -> 180461 bytes img/web-prototype.png | Bin 0 -> 23456 bytes memoria.pdf | Bin 0 -> 305752 bytes memoria.pyg | 95 ++++++++++++++++++++ memoria.tex | 91 +++++++++++++++++++ minted.sty | 239 ++++++++++++++++++++++++++++++++++++++++++++++++++ ocaml_colors.tex | 123 ++++++++++++++++++++++++++ portada/defs.tex | 25 ++++++ portada/fic.png | Bin 0 -> 241098 bytes portada/portada.png | Bin 0 -> 22317 bytes portada/portada.tex | 57 ++++++++++++ portada/upmc.png | Bin 0 -> 15449 bytes 25 files changed, 914 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100755 bib.bib create mode 100755 defs.tex create mode 100644 img/br93.png create mode 100644 img/browser-post.png create mode 100644 img/browser-pre.png create mode 100644 img/editor.png create mode 100644 img/index.png create mode 100644 img/login.png create mode 100644 img/proofs.png create mode 100644 img/register.png create mode 100644 img/results.png create mode 100644 img/web-finished.png create mode 100644 img/web-prototype.png create mode 100644 memoria.pdf create mode 100644 memoria.pyg create mode 100755 memoria.tex create mode 100644 minted.sty create mode 100644 ocaml_colors.tex create mode 100644 portada/defs.tex create mode 100644 portada/fic.png create mode 100644 portada/portada.png create mode 100644 portada/portada.tex create mode 100644 portada/upmc.png 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 Binary files /dev/null and b/img/br93.png differ diff --git a/img/browser-post.png b/img/browser-post.png new file mode 100644 index 0000000..b45eab5 Binary files /dev/null and b/img/browser-post.png differ diff --git a/img/browser-pre.png b/img/browser-pre.png new file mode 100644 index 0000000..f5849a6 Binary files /dev/null and b/img/browser-pre.png differ diff --git a/img/editor.png b/img/editor.png new file mode 100644 index 0000000..7bdfa46 Binary files /dev/null and b/img/editor.png differ diff --git a/img/index.png b/img/index.png new file mode 100644 index 0000000..e47be96 Binary files /dev/null and b/img/index.png differ diff --git a/img/login.png b/img/login.png new file mode 100644 index 0000000..586d84f Binary files /dev/null and b/img/login.png differ diff --git a/img/proofs.png b/img/proofs.png new file mode 100644 index 0000000..381db07 Binary files /dev/null and b/img/proofs.png differ diff --git a/img/register.png b/img/register.png new file mode 100644 index 0000000..60a41ea Binary files /dev/null and b/img/register.png differ diff --git a/img/results.png b/img/results.png new file mode 100644 index 0000000..c28f0d0 Binary files /dev/null and b/img/results.png differ diff --git a/img/web-finished.png b/img/web-finished.png new file mode 100644 index 0000000..3eb0e5e Binary files /dev/null and b/img/web-finished.png differ diff --git a/img/web-prototype.png b/img/web-prototype.png new file mode 100644 index 0000000..f6a5538 Binary files /dev/null and b/img/web-prototype.png differ diff --git a/memoria.pdf b/memoria.pdf new file mode 100644 index 0000000..62ab0b3 Binary files /dev/null and b/memoria.pdf differ 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 >\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 Binary files /dev/null and b/portada/fic.png differ diff --git a/portada/portada.png b/portada/portada.png new file mode 100644 index 0000000..c558fa4 Binary files /dev/null and b/portada/portada.png differ 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 Binary files /dev/null and b/portada/upmc.png differ -- cgit v1.2.3