From 6497357040adcbed045f3d89c92c6f150bffeee9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sat, 2 Dec 2017 01:34:04 +0100 Subject: [PATCH] Add missing tex-files --- proposal/chalmerstitle.sty | 56 +++++++++++++++++++++++ proposal/macros.tex | 14 ++++++ proposal/refs.bib | 94 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 164 insertions(+) create mode 100644 proposal/chalmerstitle.sty create mode 100644 proposal/macros.tex create mode 100644 proposal/refs.bib diff --git a/proposal/chalmerstitle.sty b/proposal/chalmerstitle.sty new file mode 100644 index 0000000..5a48b93 --- /dev/null +++ b/proposal/chalmerstitle.sty @@ -0,0 +1,56 @@ +% Requires: hypperref +\ProvidesPackage{chalmerstitle} + +\newcommand*{\authoremail}[1]{\gdef\@authoremail{#1}} +\newcommand*{\supervisor}[1]{\gdef\@supervisor{#1}} +\newcommand*{\supervisoremail}[1]{\gdef\@supervisoremail{#1}} +\newcommand*{\cosupervisor}[1]{\gdef\@cosupervisor{#1}} +\newcommand*{\cosupervisoremail}[1]{\gdef\@cosupervisoremail{#1}} +\newcommand*{\institution}[1]{\gdef\@institution{#1}} + +\renewcommand*{\maketitle}{% +\begin{titlepage} + + +\begin{center} + + +{\scshape\LARGE Master thesis project proposal\\} + +\vspace{0.5cm} + +{\LARGE\bfseries \@title\\} + +\vspace{2cm} + +{\Large \@author\\ \href{mailto:\@authoremail>}{\texttt{<\@authoremail>}} \\} + +% \vspace{0.2cm} +% +% {\Large name and email adress of student 2\\} + +\vspace{1.0cm} + +{\large Supervisor: \@supervisor\\ \href{mailto:\@supervisoremail>}{\texttt{<\@supervisoremail>}}\\} + +\vspace{0.2cm} + +{\large Co-supervisor: \@cosupervisor\\ \href{mailto:\@cosupervisoremail>}{\texttt{<\@cosupervisoremail>}}\\} + +\vspace{1.5cm} + +{\large Relevant completed courses:\par} +{\itshape +Logic in Computer Science\\ +Models of Computation\\ +Research topic in Computer Science\\ +Types for programs and proofs +} + +\vfill + +{\large \@institution\\\today\\} + +\end{center} +\end{titlepage} +} diff --git a/proposal/macros.tex b/proposal/macros.tex new file mode 100644 index 0000000..abf3d42 --- /dev/null +++ b/proposal/macros.tex @@ -0,0 +1,14 @@ +\newcommand*{\defeq}{\mathrel{\vcenter{\baselineskip0.5ex \lineskiplimit0pt + \hbox{\scriptsize.}\hbox{\scriptsize.}}}% + =} + +\newcommand{\defeq}{\coloneqq} +\newcommand{\bN}{\mathbb{N}} +\newcommand{\to}{\rightarrow}} +\newcommand{\mto}{\mapsto}} +\newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace} +\let\type\UU +\newcommand{\nomen}[1]{\emph{#1}} +\newcommand{\todo}[1]{\textit{#1}} +\newcommand{\comp}{\circ} +\newcommand{\x}{\times} diff --git a/proposal/refs.bib b/proposal/refs.bib new file mode 100644 index 0000000..559ab63 --- /dev/null +++ b/proposal/refs.bib @@ -0,0 +1,94 @@ +@article{cohen-2016, + author = {Cyril Cohen and + Thierry Coquand and + Simon Huber and + Anders M{\"{o}}rtberg}, + title = + { Cubical Type Theory: + a constructive interpretation of the univalence axiom + }, + journal = {CoRR}, + volume = {abs/1611.02108}, + year = {2016}, + url = {http://arxiv.org/abs/1611.02108}, + timestamp = {Thu, 01 Dec 2016 19:32:08 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CohenCHM16}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} +@book{hott-2013, + author = {The {Univalent Foundations Program}}, + title = {Homotopy Type Theory: Univalent Foundations of Mathematics}, + publisher = {\url{https://homotopytypetheory.org/book}}, + address = {Institute for Advanced Study}, + year = 2013 +} +@book{awodey-2006, + title={Category Theory}, + author={Awodey, S.}, + isbn={9780191513824}, + series={Oxford Logic Guides}, + url={https://books.google.se/books?id=IK\_sIDI2TCwC}, + year={2006}, + publisher={Ebsco Publishing} +} +@misc{cubical-demo, + author = {Andrea Vezzosi}, + title = {Cubical Type Theory Demo}, + year = {2017}, + publisher = {GitHub}, + journal = {GitHub repository}, + howpublished = {\url{https://github.com/Saizan/cubical-demo}}, + commit = {a51d5654c439111110d5b6df3605b0043b10b753} +} +@misc{cubical-agda, + author = {Andrea Vezzosi}, + title = {Cubical Extension to Agda}, + year = {2017}, + publisher = {GitHub}, + journal = {GitHub repository}, + howpublished = {\url{https://github.com/agda/agda}}, + commit = {92de32c0669cb414f329fff25497a9ddcd58b951} +} +@misc{cubical-agda, + author = {Ulf Norell}, + title = {Agda}, + year = {2017}, + publisher = {GitHub}, + journal = {GitHub repository}, + howpublished = {\url{https://github.com/agda/agda}}, + commit = {92de32c0669cb414f329fff25497a9ddcd58b951} +} +@inproceedings{bezem-2014, + title={A model of type theory in cubical sets}, + author={Bezem, Marc and Coquand, Thierry and Huber, Simon}, + booktitle={19th International Conference on Types for Proofs and Programs (TYPES 2013)}, + volume={26}, + pages={107--128}, + year={2014} +} +@article{coquand-2013, + title={Isomorphism is equality}, + author={Coquand, Thierry and Danielsson, Nils Anders}, + journal={Indagationes Mathematicae}, + volume={24}, + number={4}, + pages={1105--1120}, + year={2013}, + publisher={Elsevier} +} +@inproceedings{dybjer-1995, + title={Internal type theory}, + author={Dybjer, Peter}, + booktitle={International Workshop on Types for Proofs and Programs}, + pages={120--134}, + year={1995}, + organization={Springer} +} +@inproceedings{voevodsky-2011, + title={Univalent foundations of mathematics}, + author={Voevodsky, Vladimir}, + booktitle={International Workshop on Logic, Language, Information, and Computation}, + pages={4--4}, + year={2011}, + organization={Springer} +} \ No newline at end of file