From 357e2a087deac103af55b9ebc121cc69e9d6873a Mon Sep 17 00:00:00 2001 From: Mysaa Date: Wed, 26 Jul 2023 17:39:02 +0200 Subject: [PATCH] Started to write the report, created toc and files --- .gitignore | 1 + report/Bilibibio.bib | 30 ++++++++++++ report/M1Report.tex | 57 ++++++++++++++++++++++ report/header.tex | 110 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 198 insertions(+) create mode 100644 report/Bilibibio.bib create mode 100644 report/M1Report.tex create mode 100644 report/header.tex diff --git a/.gitignore b/.gitignore index 5afa5d4..867ffb9 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,4 @@ \#*\# .\#* *.kate-swp +/report/build/ diff --git a/report/Bilibibio.bib b/report/Bilibibio.bib new file mode 100644 index 0000000..a2a6cbc --- /dev/null +++ b/report/Bilibibio.bib @@ -0,0 +1,30 @@ +@article{RedFreeNorm1995, + doi = {10.1007/3-540-60164-3_27}, + url = {https://doi.org/10.1007\%2F3-540-60164-3_27}, + year = 1995, + publisher = {Springer Berlin Heidelberg}, + pages = {182--199}, + author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher}, + title = {Categorical reconstruction of a reduction free normalization proof}, + booktitle = {Category Theory and Computer Science} +} +@article{NBE2016, + title={Normalisation by Evaluation for Dependent Types}, + author={Thorsten Altenkirch and Ambrus Kaposi}, + booktitle={International Conference on Formal Structures for Computation and Deduction}, + year={2016} +} +@phdthesis{AltenkirschThesis1993, + title={Constructions, inductive types and strong normalization}, + author={Thorsten Altenkirch}, + booktitle={CST}, + year={1993} +} +@unpublished{TaoOfTypes, + title={The Tao of Types}, + author={Thorsten Altenkirsch} +} +@inproceedings{folSogatKaposi2023, + title={Why is equality interesting?}, + author={Ambrus Kaposi}, + url={https://akaposi.github.io/pres_wld.pdf}} \ No newline at end of file diff --git a/report/M1Report.tex b/report/M1Report.tex new file mode 100644 index 0000000..3c1d493 --- /dev/null +++ b/report/M1Report.tex @@ -0,0 +1,57 @@ +% !TeX spellcheck = fr_FR +\documentclass[10pt,a4paper]{article} + +\include{./header.tex} + +\title{Completeness Proof for different logical frameworks + \\[1ex] \large Notes on my 3 month internship at Faculty of Informatics (ELTE, Budapest)} +\hypersetup{pdftitle={Completeness Proof for different kinds of logical frameworks}} +\author{Samy Avrillon, supervised by + \\[1ex] Ambrus Kaposi (ELTE, Budapest) + \\[1ex] and Thorsten Altenkirsch (University of Notthingham, United Kingdom)} + +\begin{document} + + \doparttoc + \maketitle + + \hsep + + \tableofcontents + + \newpage + + \section{Introduction} + \subsection{Introduction to the problem} + \subsection{Motivation} + \subsection{Structure of this report} + \section{A first account of Completeness and Normalization} + \subsection{Normalization for ZOL} + \subsection{Normalization for IFOL} + \subsection{Merging the two proofs} + \section{Predicate Logic} + \subsection{SOGAT Presentation of FFOL} + \subsection{Turning a SOGAT Presentation into a GAT} + \section{Implementing the Syntax} + \subsection{Separated Contexts} + \subsection{Transport Hell} + %\section{Completeness and Normalization for FFOL} + + \section{Summary} + + + \section{Bibliography} + \begingroup + \renewcommand{\section}[2]{}% + \printbibliography + \endgroup + + \newpage + \addappheadtotoc + \appendix + \addtocontents{toc}{\protect\setcounter{tocdepth}{-1}} + \appendixpage + + \section{Agda Code} + +\end{document} diff --git a/report/header.tex b/report/header.tex new file mode 100644 index 0000000..381017e --- /dev/null +++ b/report/header.tex @@ -0,0 +1,110 @@ +% Loading packages +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{hyperref} +\hypersetup{ + colorlinks=true, + linkcolor=blue, + filecolor=magenta, + urlcolor=cyan +} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage{bbm} +\usepackage{stmaryrd} +\usepackage[main=english]{babel} +\usepackage{csquotes} +\usepackage{listings} +\usepackage{lstautogobble} +\usepackage{algorithm2e} +\usepackage{svg} +\usepackage{tikz} +\usepackage{multirow} +\usepackage{multicol} +\usepackage{tcolorbox} +\usepackage{mdframed} +\usepackage{proof} +\usepackage{biblatex} +\usepackage{xparse} +\usepackage{cprotect} +\usepackage{titlesec} +\usepackage{xpatch} +\usepackage{enumitem} +\usepackage{amsfonts} +\usepackage{mathtools} +\usepackage[page,header]{appendix} +\usepackage{minitoc} + +\usepackage{geometry} + +\usepackage{csquotes} +\usepackage[lighttt]{lmodern} +\usetikzlibrary{shapes.geometric,positioning} + +% Macros caractères globales +\newcommand{\pgrph}{\P} +\newcommand{\hsep}{\vspace{.2cm}\centerline{\rule{0.8\linewidth}{.05pt}}\vspace{.4cm}} +\renewcommand{\P}{\mathbb{P}} +\newcommand{\E}{\mathbb{E}} +\newcommand{\1}{\scalebox{1.2}{$\mathbbm{1}$}} +\newcommand{\floor}[1]{\left\lfloor#1\right\rfloor} +\newcommand{\littleO}{o} +\newcommand{\bigO}{\mathcal{O}} +\newcommand{\longdash}{\:\textrm{---}\:} +\newcommand\hole{\left[\raisebox{-0.25ex}{\scalebox{1.2}{$\cdot$}}\right]} +\newcommand\bracket[1]{\!\left[#1\right]} +\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad} +\newcommand\eng[1]{\textit{\foreignlanguage{english}{#1}}} +\newcommand\spacebar{\;|\;} +\def\nDownarrow{\not\mspace{1mu}\Downarrow} +\let\pprec\preccurlyeq + +\DeclareUnicodeCharacter{03BB}{$\lambda$} +\DeclareUnicodeCharacter{03B1}{$\alpha$} +\DeclareUnicodeCharacter{03C0}{$\pi$} + +% Création des environnement globaux +\newtheorem{theorem}{Théorème} +\newtheorem{definition}{Definition} +\newtheorem{property}{Propriété} + +\newcounter{rule} +\addto\extrasfrench{% + \renewcommand{\figureautorefname}{\textsc{Figure}} + \renewcommand{\sectionautorefname}{Section} + \renewcommand{\subsectionautorefname}{Sous-section} + \renewcommand{\appendixautorefname}{Annexe} + \renewcommand{\theoremautorefname}{Théorème} + \providecommand\propertyautorefname{Propriété} + \providecommand\ruleautorefname{règle} +} + +% Commandes logiques globales +\newcommand{\ifnullthenelse}[3]{ + \ifnum\value{#1}=0 + #2 + \else + #3 + \fi +} + +%%% Commande \newtag permettant de changer le label d'une equation +\makeatletter +\newcommand\newtag[2]{#1\def\@currentlabel{#1}\label{#2}} +\makeatother + + +% Macros caractères spécifiques au document + +% Création des environnements spécifiques au document + + +%%% Subparaghaphs box +\newtcbox{\subparaghaphbox}{nobeforeafter,tcbox raise base, arc=9pt, outer arc=9pt, boxsep=2pt,left=2pt,right=2pt,top=2pt,bottom=2pt,boxrule=1pt,colback=white!85!orange} +\newcommand{\subparaghaphboxedcontent}[1]{\subparaghaphbox{#1}\newline} +%\titleclass{\mathcases}{straight}[\subparagraph] +\titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent} +\titlespacing*{\subparagraph}{0pt}{3.25ex plus 1ex minus .2ex}{0.5em} + + +\addbibresource{Bilibibio.bib}