Add missing tex-files
This commit is contained in:
parent
35c246f17d
commit
6497357040
56
proposal/chalmerstitle.sty
Normal file
56
proposal/chalmerstitle.sty
Normal file
|
|
@ -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}
|
||||
}
|
||||
14
proposal/macros.tex
Normal file
14
proposal/macros.tex
Normal file
|
|
@ -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}
|
||||
94
proposal/refs.bib
Normal file
94
proposal/refs.bib
Normal file
|
|
@ -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}
|
||||
}
|
||||
Loading…
Reference in a new issue