<commit_before>\documentclass[preprint, authoryear]{sigplanconf}

\usepackage{amsmath}
\usepackage{verbatim}

\include{macros}

%% Structure
\newenvironment{structure}{\footnotesize\verbatim}{\endverbatim}
%\newenvironment{structure}{\comment}{\endcomment}


\begin{document}

%\conferenceinfo{WXYZ '05}{date, City.} 
%\copyrightyear{2005} 
%\copyrightdata{[to be supplied]} 

%\titlebanner{banner above paper title}        % These are ignored unless
%\preprintfooter{short description of paper}   % 'preprint' option specified.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Title
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\title{The Gentle Art of Levitation}
% Or something mentionning levitation. Feel free to change. 
% \subtitle{Subtitle Text, if any}


%% Alphabetical ordering.
\authorinfo{<NAME>}
           {Institute of Cybernetics, Tallinn University of Technology}
           {<EMAIL>}
\authorinfo{Pierre-\'{<NAME> \\ <NAME>}
           {University of Strathclyde}
           {\{<EMAIL>,<EMAIL>}
\authorinfo{<NAME>}
           {University of Nottingham}
           {<EMAIL>}


\maketitle


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Abstract
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{abstract}
This is the text of the abstract.
\end{abstract}

%\category{CR-number}{subcategory}{third-level}

%\terms
%term1, term2

%\keywords
%keyword1, keyword2





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Introduction
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}

The text of the paper begins here. \cite{morris:spf}

ACM bullet points, we offer:
\begin{itemize}
\item a closed presentation of data-types (no generativity requires)
  subsuming standard inductive families (some popular extensions
  excluded for now)
\item descriptions of data-types are first-class (indeed,
  self-encoded)
\item ``generic programming is just programming''
\item first serious attempt to design a language for generic
  programming, except possibly Lisp
\end{itemize}

\begin{structure}
<- presentation of the Core theory
    -> judgemental equality (extensional (a la OTT?))
    /> not Epigram specific 
        <- having OTT just buys you more stuffs
\end{structure}

\newcommand{\Valid}{\textsc{valid}}
\newcommand{\Set}{\textsc{Set}}
\newcommand{\Type}[1]{{#1}:\Set}
\newcommand{\x}{x}
\newcommand{\bnd}[2]{{#1}\!:\!{#2}}
\newcommand{\xS}{\bnd{x}{S}}
\newcommand{\stkl}[1]{\begin{array}[b]{@{}l@{}}#1\end{array}}
\newcommand{\stkc}[1]{\begin{array}[b]{@{}c@{}}#1\end{array}}
\newcommand{\pr}[2]{\left[{#1},{#2}\right]}

\[
\begin{array}{ll}
\Gamma\vdash\Valid & \mbox{\(\Gamma\) is a valid context, giving types to
                    variables} \\
\Gamma\vdash t:T & \mbox{term \(t\) has type \(T\) in context \(\Gamma\)} \\
\Gamma\vdash s\equiv t : T & \mbox{\(s\) and \(t\) are equal at type \(T\)
   in context \(\Gamma\)} \\
\end{array}
\]

The systems of inference rules will be formulated to ensure that that the
following implications always hold by induction on derivations.
\[\begin{array}{l@{\;\;\Rightarrow\;\;}l}
\Gamma\vdash t:T & \Gamma\vdash\Valid \;\wedge\; \Gamma\vdash\Type{T} \\
\Gamma\vdash s\equiv t:T & \Gamma\vdash s:T \;\wedge\; \Gamma\vdash t:T \\
\Gamma;\xS;\Delta \vdash J &
  \Gamma\vdash s:S \;\Rightarrow\; \Gamma;\Delta[s/x] \vdash J[s/x] \\
\end{array}\]


\[
\Axiom{\vdash\Valid}\qquad
\Rule{\Gamma\vdash\Type{S}}
     {\Gamma;\xS\vdash\Valid}\;x\not\in\Gamma
\]

\[\stkc{\stkl{
\Rule{\Gamma\vdash\Valid}
     {\Gamma\vdash\Type{\Set}}\qquad
\Rule{\Gamma\vdash\Type{S}\quad\Gamma,\xS\vdash\Type{T}}
     {\Gamma\vdash\Type{(\xS)\to T, (\xS)\times T} }}
}\]

\[
\Rule{\Gamma;\xS;\Delta\vdash\Valid}
     {\Gamma;\xS;\Delta\vdash x:S}\qquad
\Rule{\Gamma\vdash s:S \quad \Gamma\vdash\Type{S\equiv T}}
     {\Gamma\vdash s:T}
\]

\[
\Rule{\stkl{\Gamma\vdash\Type{S}\\\Gamma;\xS\vdash t:T}}
     {\Gamma\vdash \lambda_S x.\,t:(\xS)\to T} \qquad
\Rule{\stkl{\Gamma\vdash f:(\xS)\to T \\
      \Gamma\vdash s:S}}
     {\Gamma\vdash f\:s \vdash T[s/x]} 
\]

\[
\Rule{\stkl{\Gamma\vdash\Type{S}\quad\Gamma;\xS\vdash t:T\\
      \Gamma\vdash s:S}}
     {\Gamma\vdash (\lambda_S x.\,t)\:s \equiv t[s/x] \vdash T[s/x]} 
\]
\[
\Rule{\Gamma\vdash s:S \quad \Gamma;\xS\vdash\Type{T}\quad
      \Gamma\vdash t:T[s/x]}
     {\Gamma\vdash \pr{s}{t}_{x.T} : (\xS)\times T}
\]

\[
\Rule{\Gamma\vdash p:(\xS)\times T}
     {\Gamma\vdash \pi_0 p : S} \qquad
\Rule{\Gamma\vdash p:(\xS)\times T}
     {\Gamma\vdash \pi_1 p : T[\pi_0 p/x]}
\]


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Desc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{A simple universe of descriptions}

\begin{structure}
<- a universe of simple inductive types
    -> nil, arg, ind, hind
<- levitation
\end{structure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% IDesc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Indexing descriptions}


\begin{structure}
<- enumerations
<- indexing
    -> nil, arg, ind, hind
    -> var, Pi, Sigma, :-, x, Sigma_f
<- closure under \box and \diamond<commit_msg>Desc@ICFP: add minimal Prop to the base theory.<commit_after>\documentclass[preprint, authoryear]{sigplanconf}

\usepackage{amsmath}
\usepackage{verbatim}

\include{macros}

%% Structure
\newenvironment{structure}{\footnotesize\verbatim}{\endverbatim}
%\newenvironment{structure}{\comment}{\endcomment}


\begin{document}

%\conferenceinfo{WXYZ '05}{date, City.} 
%\copyrightyear{2005} 
%\copyrightdata{[to be supplied]} 

%\titlebanner{banner above paper title}        % These are ignored unless
%\preprintfooter{short description of paper}   % 'preprint' option specified.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Title
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\title{The Gentle Art of Levitation}
% Or something mentionning levitation. Feel free to change. 
% \subtitle{Subtitle Text, if any}


%% Alphabetical ordering.
\authorinfo{<NAME>}
           {Institute of Cybernetics, Tallinn University of Technology}
           {<EMAIL>}
\authorinfo{Pierre-\'{E}<NAME> \\ <NAME>}
           {University of Strathclyde}
           {\{<EMAIL>,<EMAIL>}
\authorinfo{<NAME>}
           {University of Nottingham}
           {<EMAIL>}


\maketitle


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Abstract
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{abstract}
This is the text of the abstract.
\end{abstract}

%\category{CR-number}{subcategory}{third-level}

%\terms
%term1, term2

%\keywords
%keyword1, keyword2





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Introduction
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}

The text of the paper begins here. \cite{morris:spf}

ACM bullet points, we offer:
\begin{itemize}
\item a closed presentation of data-types (no generativity requires)
  subsuming standard inductive families (some popular extensions
  excluded for now)
\item descriptions of data-types are first-class (indeed,
  self-encoded)
\item ``generic programming is just programming''
\item first serious attempt to design a language for generic
  programming, except possibly Lisp
\end{itemize}

\begin{structure}
<- presentation of the Core theory
    -> judgemental equality (extensional (a la OTT?))
    /> not Epigram specific 
        <- having OTT just buys you more stuffs
\end{structure}

\newcommand{\Valid}{\textsc{valid}}
\newcommand{\Set}{\textsc{Set}}
\newcommand{\Type}[1]{{#1}:\Set}
\newcommand{\x}{x}
\newcommand{\bnd}[2]{{#1}\!:\!{#2}}
\newcommand{\xS}{\bnd{x}{S}}
\newcommand{\stkl}[1]{\begin{array}[b]{@{}l@{}}#1\end{array}}
\newcommand{\stkc}[1]{\begin{array}[b]{@{}c@{}}#1\end{array}}
\newcommand{\pr}[2]{\left[{#1},{#2}\right]}

\newcommand{\Prop}{\textsc{Prop}}
\newcommand{\prf}[1]{{:\!\!-}~#1}
\newcommand{\True}{\mathsf{TT}}


\subsection{Base theory}

\[
\begin{array}{ll}
\Gamma\vdash\Valid & \mbox{\(\Gamma\) is a valid context, giving types to
                    variables} \\
\Gamma\vdash t:T & \mbox{term \(t\) has type \(T\) in context \(\Gamma\)} \\
\Gamma\vdash s\equiv t : T & \mbox{\(s\) and \(t\) are equal at type \(T\)
   in context \(\Gamma\)} \\
\end{array}
\]

The systems of inference rules will be formulated to ensure that that the
following implications always hold by induction on derivations.
\[\begin{array}{l@{\;\;\Rightarrow\;\;}l}
\Gamma\vdash t:T & \Gamma\vdash\Valid \;\wedge\; \Gamma\vdash\Type{T} \\
\Gamma\vdash s\equiv t:T & \Gamma\vdash s:T \;\wedge\; \Gamma\vdash t:T \\
\Gamma;\xS;\Delta \vdash J &
  \Gamma\vdash s:S \;\Rightarrow\; \Gamma;\Delta[s/x] \vdash J[s/x] \\
\end{array}\]


\[
\Axiom{\vdash\Valid}\qquad
\Rule{\Gamma\vdash\Type{S}}
     {\Gamma;\xS\vdash\Valid}\;x\not\in\Gamma
\]

\[\stkc{\stkl{
\Rule{\Gamma\vdash\Valid}
     {\Gamma\vdash\Type{\Set}}\qquad
\Rule{\Gamma\vdash\Type{S}\quad\Gamma,\xS\vdash\Type{T}}
     {\Gamma\vdash\Type{(\xS)\to T, (\xS)\times T} }}
}\]

\[
\Rule{\Gamma;\xS;\Delta\vdash\Valid}
     {\Gamma;\xS;\Delta\vdash x:S}\qquad
\Rule{\Gamma\vdash s:S \quad \Gamma\vdash\Type{S\equiv T}}
     {\Gamma\vdash s:T}
\]

\[
\Rule{\stkl{\Gamma\vdash\Type{S}\\\Gamma;\xS\vdash t:T}}
     {\Gamma\vdash \lambda_S x.\,t:(\xS)\to T} \qquad
\Rule{\stkl{\Gamma\vdash f:(\xS)\to T \\
      \Gamma\vdash s:S}}
     {\Gamma\vdash f\:s \vdash T[s/x]} 
\]

\[
\Rule{\stkl{\Gamma\vdash\Type{S}\quad\Gamma;\xS\vdash t:T\\
      \Gamma\vdash s:S}}
     {\Gamma\vdash (\lambda_S x.\,t)\:s \equiv t[s/x] \vdash T[s/x]} 
\]

\[
\Rule{\Gamma\vdash s:S \quad \Gamma;\xS\vdash\Type{T}\quad
      \Gamma\vdash t:T[s/x]}
     {\Gamma\vdash \pr{s}{t}_{x.T} : (\xS)\times T}
\]

\[
\Rule{\Gamma\vdash p:(\xS)\times T}
     {\Gamma\vdash \pi_0 p : S} \qquad
\Rule{\Gamma\vdash p:(\xS)\times T}
     {\Gamma\vdash \pi_1 p : T[\pi_0 p/x]}
\]

\[
\Rule{\Gamma\vdash q : \Prop}
     {\Gamma\vdash \prf{q} : \Set}\qquad
\Rule{\Gamma \vdash \Valid}
     {\Gamma \vdash \True : \Prop}
\]


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Desc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{A simple universe of descriptions}

\begin{structure}
<- a universe of simple inductive types
    -> nil, arg, ind, hind
<- levitation
\end{structure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% IDesc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Indexing descriptions}


\begin{structure}
<- enumerations
<- indexing
    -> nil, arg, ind, hind
    -> var, Pi, Sigma, :-, x, Sigma_f
<- closure under \box and \diamond
{'fraction_non_alphanumeric': 0.29141217841939665, 'fraction_numerical': 0.004812141402924301, 'mean_word_length': 3.8245535714285714, 'pattern_counts': {'":': 0, '<': 33, '<?xml version=': 0, '>': 29, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1859252', 'n_tokens_mistral': 3814, 'n_tokens_neox': 3564, 'n_words': 784}