Stefan pushed to branch report/els-2017 at Stefan / Typer

Commits: 678efd2a by Stefan Monnier at 2017-01-29T21:34:28-05:00 -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -175,6 +175,8 @@ of syntactic categories and generally make ``everything'' first-class. \keywords{Macros, S-expressions, Pure Type Systems, ML, Lisp}

\maketitle +\renewcommand \shortauthors { + P. Delaunay, V. Archamboult-Bouffard, and S. Monnier}

\section{Introduction}

@@ -290,22 +292,6 @@ explicitly quoting the macro's arguments (e.g.~passing them as strings), making the macro calls more verbose, and the macro itself harder to implement since you have to manually parse those quoted arguments.

-%% \begin{figure} -%% \begin{displaymath} -%% \MAlign{ -%% \kw{type}~\id{Lexp} \ -%% ~~|~\id{var}~\id{Id} \ -%% ~~|~\id{app}~\id{Lexp}~(\id{List}~\id{Lexp}) \ -%% ~~|~\id{fun}~(\id{List}~\id{Id})~\id{Lexp} \ -%% ~~|~\id{let}~\id{Id}~\id{Lexp}~\id{Lexp} \ -%% ~~|~\id{case}~\id{Lexp}~(\id{List}~\id{Lbranch}) \ -%% ~~~\ldots -%% } -%% \end{displaymath} -%% \label{fig:Lexp} -%% \caption{Definition of $\lambda$-expressions} -%% \end{figure} - Of course, it should be noted that the rest of the world re-discovered the power of S-expressions under the name of XML, where it is used for similar reasons: this intermediate parsing stage is a convenient compromise, since @@ -679,6 +665,25 @@ it was natural and important to be able to distinguish those two cases. \section{Elaboration to core Typer} \label{sec:elaboration}

+\begin{figure} + \begin{displaymath} + \MAlign{ + \kw{type}~\id{Lexp} \ + ~~|~\id{var}~\id{Id} \ + ~~|~\id{app}~\id{Lexp}~(\id{List}~\id{Lexp}) \ + ~~|~\id{fun}~(\id{List}~\id{Id})~\id{Lexp} \ + ~~|~\id{let}~\id{Id}~\id{Lexp}~\id{Lexp} \ + ~~|~\id{case}~\id{Lexp}~(\id{List}~\id{Lbranch}) \ + ~~~\ldots + } + \end{displaymath} + \label{fig:Lexp} + \caption{Definition of $\lambda$-expressions} +\end{figure} + +No hard coded names: just initial bindings of constructs to special forms +and primitive functions. + Macros recognized by the type \kw{Macro}.

Bidirectional type checking. @@ -716,6 +721,9 @@ Coq~\cite{Coq00} \section{Conclusion and future work} \label{sec:conclusion}

+Implementation in progress, available from +\url{http://gitlab.com/monnier/typer%7D. + \begin{acks} The work is supported by the \grantsponsor{NSERC}{National Science and Engineering Research of Canada}

View it on GitLab: https://gitlab.com/monnier/typer/commit/678efd2a7dab4a7cce341592ec13f4a97d9e...