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

Commits: 982f07e3 by Stefan Monnier at 2017-01-29T21:13:18-05:00 -

- - - - -

2 changed files:

- paper.tex - all.bib → refs.bib

Changes:

===================================== paper.tex ===================================== --- a/paper.tex +++ b/paper.tex @@ -622,6 +622,8 @@ is parsed into the following S-expression: nil (cons a (List a))) \end{verbatim} +Because \id{type} is defined as a prefix operator, and $\mid$ is defined as +an associative infix operator.

\subsection{Two-level tokenizing} @@ -677,6 +679,23 @@ it was natural and important to be able to distinguish those two cases. \section{Elaboration to core Typer} \label{sec:elaboration}

+Macros recognized by the type \kw{Macro}. + +Bidirectional type checking. + +Lexically scoped macros. + +No notion of phase level for bindings~\cite{Flatt02}: instead, when a macro +call is found, the macro definition needs to be \emph{closed} and its +dependencies are all evaluated. Since Typer is pure, these evaluations have +no effect and their results can be cached. + +Interleaved type checking/inference and macro expansion. + +Access to the typing environment and expected type of returned code +(i.e. hypotheses and goal, when seen from the point of view of a proof +assistant). + \section{Related work} \label{sec:related}

@@ -708,8 +727,7 @@ Coq~\cite{Coq00}

%% \bibliographystyle{alpha} \bibliographystyle{ACM-Reference-Format} -\bibliography{all.bib} -%% \bibliography{refs.bib} +\bibliography{refs.bib}

\end{document}

===================================== all.bib → refs.bib ===================================== --- a/all.bib +++ b/refs.bib @@ -2359,6 +2359,32 @@ toiti crossref = {PLDI93}, pages = "237-247" } +@InProceedings{Flatt02, + author = Flatt, + title = {Composable and Compilable Macros: You Want it When?}, + crossref = {ICFP02}, + pages = {72-83}, + url = {http://dl.acm.org/citation.cfm?id=581486%7D, + abstract = {Many macro systems, especially for Lisp and Scheme, allow + macro transformers to perform general computation. + Moreover, the language for implementing compile-time macro + transformers is usually the same as the language for + implementing run-time functions. As a side effect of this + sharing, implementations tend to allow the mingling of + compile-time values and run-time values, as well as values + from separate compilations. Such mingling breaks + programming tools that must parse code without executing + it. Macro implementors avoid harmful mingling by obeying + certain macro-definition protocols and by inserting + phase-distinguishing annotations into the code. However, + the annotations are fragile, the protocols are not + enforced, and programmers can only reason about the result + in terms of the compiler's implementation. MzScheme---the + language of the PLT Scheme tool suite---addresses the + problem through a macro system that separates compilation + without sacrificing the expressiveness of macros.} +} + @Article{Floyd63, author = {Robert W. Floyd}, title = {Syntactic Analysis and Operator Precedence}, @@ -6920,6 +6946,15 @@ toiti publisher = ACM, address = {Florence, Italy} } +@Proceedings{ICFP02, + title = ICFP, + booktitle = ICFP, + year = 2002, + key = {ICFP'02}, + month = oct, + publisher = ACM, + address = {Pittsburgh, PA} +} @Proceedings{ICFP03, title = ICFP, booktitle = ICFP,

View it on GitLab: https://gitlab.com/monnier/typer/commit/982f07e33d6366997776f51af92be46d5150...