Stefan pushed to branch report/itd at Stefan / Typer

Commits: 04cd7486 by Stefan Monnier at 2018-11-02T21:16:45Z -

- - - - -

3 changed files:

- + GNUmakefile - paper.tex - + refs.bib

Changes:

===================================== GNUmakefile ===================================== @@ -0,0 +1,12 @@ +GLOBALREFS=~/share/misc/all +LOCALREFS=refs.bib +PAPER=paper + +${LOCALREFS}: ${PAPER}.aux ${GLOBALREFS}.bib + @# The -r option breaks with names with slashes :-( ! + @# bibexport -r ${GLOBALREFS} -o $@ ${PAPER}.aux + @sed 's|^\bibdata{.*}|\bibdata{${GLOBALREFS}}|' <${PAPER}.aux >${PAPER}.tmp.aux + bibexport -o $@ ${PAPER}.tmp.aux + @rm -f ${PAPER}.tmp.aux $@-save-[1-9]* + +

===================================== paper.tex ===================================== @@ -1690,5 +1690,5 @@ judgments into the logic:

\bibliographystyle{alpha} %% \bibliography{typer_theory} -\bibliography{/u/monnier/share/misc/all} +\bibliography{refs} \end{document}

===================================== refs.bib ===================================== @@ -0,0 +1,575 @@ + + +@misc{Coq00, + author = {Gérard P. Huet and Christine Paulin-Mohring and + others}, + howpublished = {Part of the Coq system version 6.3.1}, + month = may, + title = {The {Coq} Proof Assistant Reference Manual}, + year = {2000}, +} + +@inproceedings{Bove09, + author = {Ana Bove and Peter Dybjer and Ulf Norell}, + booktitle = {International Conference on Theorem Proving in + Higher-Order Logics}, + key = {TPHOLs09}, + month = aug, + pages = {73-78}, + series = {Lecture Notes in Computer Science}, + title = {A Brief Overview of {A}gda – A Functional Language + with Dependent Types}, + volume = {5674}, + year = {2009}, + abstract = {We give an overview of Agda, the latest in a series + of dependently typed programming languages developed + in Gothenburg. Agda is based on Martin-Löf’s + intuitionistic type theory but extends it with + numerous programming language features. It supports a + wide range of inductive data types, including + inductive families and inductive-recursive types, + with associated flexible pattern-matching. Unlike + other proof assistants, Agda is not tactic-based. + Instead it has an Emacs-based interface which allows + programming by gradual refinement of incomplete + type-correct terms.}, + url = {http://www.cse.chalmers.se/~ulfn/papers/tphols09/ + tutorial.pdf}, +} + +@article{Brady13, + author = {Edwin Brady}, + journal = {Journal of Functional Programming}, + number = {5}, + pages = {552-593}, + title = {Idris, a general-purpose dependently typed + programming language: Design and implementation}, + volume = {23}, + year = {2013}, + abstract = {Many components of a dependently typed programming + language are by now well understood, for example, the + underlying type theory, type checking, unification + and evaluation. How to combine these components into + a realistic and usable high-level language is, + however, folklore, discovered anew by successive + language implementors. In this paper, I describe the + implementation of Idris, a new dependently typed + functional programming language. Idris is intended to + be a general-purpose programming language and as such + provides high-level concepts such as implicit syntax, + type classes and do notation. I describe the + high-level language and the underlying type theory, + and present a tactic-based method for elaborating + concrete high-level syntax with implicit arguments + and type classes into a fully explicit type theory. + Furthermore, I show how this method facilitates the + implementation of new high-level language + constructs.}, + url = {https://eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf%7D, +} + +@inproceedings{Swamy16, + author = {Nikhil Swamy and Cătălin Hriţcu and Chantal Keller and + Aseem Rastogi and Antoine Delignat-Lavaud and + Simon Forest and Karthikeyan Bhargavan and + Cédric Fournet and Pierre-Yves Strub and + Markulf Kohlweiss and Jean-Karim Zinzindohoue and + Santiago Zanella-Béguelin}, + booktitle = {Symposium on Principles of Programming Languages}, + key = {POPL'16}, + month = jan, + pages = {256-270}, + publisher = {ACM Press}, + title = {Dependent Types and Multi-monadic Effects in {F*}}, + year = {2016}, + abstract = {We present a new, completely redesigned, version of + F*, a language that works both as a proof assistant + as well as a general-purpose, verification-oriented, + effectful programming language. In support of these + complementary roles, F* is a dependently typed, + higher-order, call-by-value language with _primitive_ + effects including state, exceptions, divergence and + IO. Although primitive, programmers choose the + granularity at which to specify effects by equipping + each effect with a monadic, predicate transformer + semantics. F* uses this to efficiently compute + weakest preconditions and discharges the resulting + proof obligations using a combination of SMT solving + and manual proofs. Isolated from the effects, the + core of F* is a language of pure functions used to + write specifications and proof terms---its + consistency is maintained by a semantic termination + check based on a well-founded order. We evaluate our + design on more than 55,000 lines of F* we have + authored in the last year, focusing on three main + case studies. Showcasing its use as a general-purpose + programming language, F* is programmed (but not + verified) in F*, and bootstraps in both OCaml and F#. + Our experience confirms F*'s pay-as-you-go cost + model: writing idiomatic ML-like code with no finer + specifications imposes no user burden. As a + verification-oriented language, our most significant + evaluation of F* is in verifying several key modules + in an implementation of the TLS-1.2 protocol + standard. For the modules we considered, we are able + to prove more properties, with fewer annotations + using F* than in a prior verified implementation of + TLS-1.2. Finally, as a proof assistant, we discuss + our use of F* in mechanizing the metatheory of a + range of lambda calculi, starting from the simply + typed lambda calculus to System F-omega and even + micro-F*, a sizeable fragment of F* itself---these + proofs make essential use of F*'s flexible + combination of SMT automation and constructive + proofs, enabling a tactic-free style of programming + and proving at a relatively large scale.}, + url = {https://dl.acm.org/citation.cfm?id=2837655%7D, +} + +@inproceedings{Casinghino14, + author = {Chris Casinghino and Vilhelm Sjöberg and + Stephanie Weirich}, + booktitle = {Symposium on Principles of Programming Languages}, + key = {POPL'14}, + pages = {33-45}, + publisher = {ACM Press}, + title = {Combining proofs and programs in a dependently typed + language}, + year = {2014}, + abstract = {Most dependently-typed programming languages either + require that all expressions terminate (e.g. Coq, + Agda, and Epigram), or allow infinite loops but are + inconsistent when viewed as logics (e.g. Haskell, + ATS, Ωmega). Here, we combine these two approaches + into a single dependently-typed core language. The + language is composed of two fragments that share a + common syntax and overlapping semantics: a logic that + guarantees total correctness, and a call-by-value + programming language that guarantees type safety but + not termination. The two fragments may interact: + logical expressions may be used as programs; the + logic may soundly reason about potentially + nonterminating programs; programs can require logical + proofs as arguments; and "mobile" program values, + including proofs computed at runtime, may be used as + evidence by the logic. This language allows + programmers to work with total and partial functions + uniformly, providing a smooth path from functional + programming to dependently-typed programming.}, + url = {https://dl.acm.org/citation.cfm?id=2535883%7D, +} + +@inproceedings{Paulin93, + author = {Christine {Paulin-Mohring}}, + booktitle = {International conference on Typed Lambda Calculi and + Applications}, + editor = {M. Bezem and J. Groote}, + key = {TLCA'93}, + month = mar, + pages = {328-345}, + publisher = {LNCS 664, Springer-Verlag}, + title = {Inductive definitions in the system {Coq}---rules and + properties}, + year = {1993}, + url = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR1992/RR1992- + 49.ps.Z}, +} + +@techreport{Gimenez94, + author = {Eduardo Giménez}, + institution = {École Normale Supérieure de Lyon}, + number = {RR1995-07}, + title = {Codifying guarded definitions with recursive schemes}, + year = {1994}, + abstract = {We formalize an extension of the Calculus of + Constructions with inductive and coinductive types + which allows a more direct description of recursive + definitions. The approach we follow is close to the + one proposed by Thierry Coquand for Martin-Loef's + type theory in his paper ``Infinite Objects in Type + Theory''. Recursive objects can be defined by + fixed-point definitions as in functional programming + languages, and a syntactical checking of these + definitions avoids the introduction of + non-normalizable terms. We show that the conditions + for accepting a recursive definition proposed in the + mentioned paper are not sufficient for the Calculus + of Constructions, and we modify them. As a way of + justifying our conditions, we develop a general + method to codify a fix point definition satisfying + them using well-known recursive schemes, like + primitive recursion and co-recursion. We also propose + different reduction rules from the ones used in [5] + in order to obtain a decidable conversion relation + for the system.}, + url = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR1995/RR1995- + 07.ps.Z}, +} + +@book{Milner97, + address = {Cambridge, Massachusetts}, + author = {Robin Milner and Mads Tofte and Robert Harper and + David B. MacQueen}, + publisher = {MIT Press}, + title = {The Definition of {S}tandard {ML} Revised}, + year = {1997}, +} + +@inproceedings{Shao97, + author = {Zhong Shao}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'97}, + month = jun, + pages = {85-98}, + publisher = {ACM Press}, + title = {Flexible Representation Analysis}, + year = {1997}, +} + +@inproceedings{Leroy92, + author = {Xavier Leroy}, + booktitle = {Symposium on Principles of Programming Languages}, + key = {POPL'92}, + month = jan, + pages = {177-188}, + title = {Unboxed Objects and Polymorphic Typing}, + year = {1992}, + abstract = {This paper presents a program transformation that + allows languages with polymorphic typing (e.g. ML) to + be implemented with unboxed, multi-word data + representations, more efficient than the conventional + boxed representations. The transformation introduces + coercions between various representations, based on a + typing derivation. A prototype ML compiler utilizing + this transformation demonstrates important speedups.}, +} + +@inproceedings{Leroy97, + author = {Xavier Leroy}, + booktitle = {International Workshop on Types in Compilation}, + key = {TIC'97}, + month = jun, + note = {BCCS-97-03}, + title = {The Effectiveness of Type-Based Unboxing}, + year = {1997}, + abstract = {We compare the efficiency of type-based unboxing + strategies with that of simpler, untyped unboxing + optimizations, building on our practical experience + with the Gallium and Objective Caml compilers. We + find the untyped optimizations to perform as well on + the best case and significantly better in the worst + case.}, +} + +@article{Barendregt91b, + author = {Henk P. Barendregt}, + journal = {Journal of Functional Programming}, + month = apr, + number = {2}, + pages = {121-154}, + title = {Introduction to generalized type systems}, + volume = {1}, + year = {1991}, + abstract = {Programming languages often come with type systems. + Some of these are simple, others are sophisticated. + As a stylistic representation of types in programming + languages several versions of typed lambda calculus + are studied. During the last 20 years many of these + systems have appeared, so there is some need of + classification. Working towards a taxonomy, + Barendregt (1991) gives a fine-structure of the + theory of constructions (Coquand and Huet 1988) in + the form of a canonical cube of eight type systems + ordered by inclusion. Berardi (1988) and Terlouw + (1988) have independently generalized the method of + constructing systems in the λ-cube. Moreover, + Berardi (1988, 1990) showed that the generalized type + systems are flexible enough to describe many logical + systems. In that way the well-known + propositions-as-types interpretation obtains a nice + canonical form.}, + url = {http://www.jeremyherve.net/bar91.pdf%7D, +} + +@inproceedings{Luo89, + author = {Zhaohui Luo}, + booktitle = {Annual Symposium on Logic in Computer Science}, + key = {LICS'89}, + pages = {386-395}, + title = {ECC, an extended calculus of constructions}, + year = {1989}, +} + +@inproceedings{Coquand92, + author = {Thierry Coquand}, + booktitle = {Workshop on Types for Proofs and Programs}, + pages = {66-79}, + title = {Pattern Matching with Dependent Types}, + year = {1992}, +} + +@inproceedings{Blume06, + address = {Portland, Oregon}, + author = {Matthias Blume and Umut A. Acar and Wonseok Chae}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'06}, + month = sep, + pages = {239-250}, + title = {Extensible programming with first-class cases}, + year = {2006}, + abstract = {We present language mechanisms for polymorphic, + extensible records and their exact dual, polymorphic + sums with extensible first-class cases. These + features make it possible to easily extend existing + code with new cases. In fact, such extensions do not + require any changes to code that adheres to a + particular programming style. Using that style, + individual extensions can be written independently + and later be composed to form larger components. + These language mechanisms provide a solution to the + expression problem. We study the proposed mechanisms + in the context of an implicitly typed, purely + functional language PolyR. We give a type system for + the language and provide rules for a 2-phase + transformation: first into an explicitly typed + λ-calculus with record polymorphism, and finally to + efficient index-passing code. The first phase + eliminates sums and cases by taking advantage of the + duality with records. We implement a version of PolyR + extended with imperative features and pattern + matching - we call this language MLPolyR. Programs in + MLPolyR require no type annotations - the + implementation employs a reconstruction algorithm to + infer all types. The compiler generates machine code + (currently for PowerPC) and optimizes the + representation of sums by eliminating closures + generated by the dual construction.}, + url = {https://dl.acm.org/citation.cfm?id=1159836%7D, +} + +@inproceedings{Castagna16, + author = {Giuseppe Castagna and Tommaso Petrucciani and + Kim Nguyên}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'16}, + month = sep, + pages = {378-391}, + title = {Set-theoretic types for polymorphic variants}, + year = {2016}, + abstract = {Polymorphic variants are a useful feature of the + OCaml language whose current definition and + implementation rely on kinding constraints to + simulate a subtyping relation via unification. This + yields an awkward formalization and results in a type + system whose behaviour is in some cases unintuitive + and/or unduly restrictive. In this work, we present + an alternative formalization of polymorphic variants, + based on set-theoretic types and subtyping, that + yields a cleaner and more streamlined system. Our + formalization is more expressive than the current one + (it types more programs while preserving type + safety), it can internalize some meta-theoretic + properties, and it removes some pathological cases of + the current implementation resulting in a more + intuitive and, thus, predictable type system. More + generally, this work shows how to add full-fledged + union types to functional languages of the ML family + that usually rely on the Hindley-Milner type system. + As an aside, our system also improves the theory of + semantic subtyping, notably by proving completeness + for the type reconstruction algorithm.}, + url = {https://dl.acm.org/citation.cfm?id=2951928%7D, +} + +@inproceedings{Chapman10, + address = {Baltimore, MD}, + author = {James Chapman and Pierre-{'E}variste Dagand and + Connor McBride and Peter Morris}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'10}, + month = sep, + pages = {3-14}, + title = {The Gentle Art of Levitation}, + year = {2010}, + abstract = {We present a closed dependent type theory whose + inductive types are given not by a scheme for + generative declarations, but by encoding in a + universe. Each inductive datatype arises by + interpreting its description - a first-class value in + a datatype of descriptions. Moreover, the latter + itself has a description. Datatype-generic + programming thus becomes ordinary programming. We + show some of the resulting generic operations and + deploy them in particular, useful ways on the + datatype of datatype descriptions itself. Simulations + in existing systems suggest that this apparently + self-supporting setup is achievable without paradox + or infinite regress.}, +} + +@inproceedings{Christiansen16, + author = {David Christiansen and Edwin Brady}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'16}, + month = sep, + pages = {284-297}, + title = {Elaborator Reflection: Extending {I}dris in {I}dris}, + year = {2016}, + abstract = {Many programming languages and proof assistants are + defined by elaboration from a high-level language + with a great deal of implicit information to a highly + explicit core language. In many advanced languages, + these elaboration facilities contain powerful tools + for program construction, but these tools are rarely + designed to be repurposed by users. We describe + elaborator reflection, a paradigm for metaprogramming + in which the elaboration machinery is made directly + available to metaprograms, as well as a concrete + realization of elaborator reflection in Idris, a + functional language with full dependent types. We + demonstrate the applicability of Idris’s reflected + elaboration framework to a number of realistic + problems, we discuss the motivation for the specific + features of its design, and we explore the broader + meaning of elaborator reflection as it can relate to + other languages.}, + url = {https://eb.host.cs.st-andrews.ac.uk/drafts/elab- + reflection.pdf}, +} + +@inproceedings{Firsov18, + author = {Denis Firsov and Aaron Stump}, + booktitle = {Certified Programs and Proofs}, + pages = {215-227}, + title = {Generic Derivation of Induction for Impredicative + Encodings in Cedille}, + year = {2018}, + abstract = {This paper presents generic derivations of induction + for impredicatively typed lambda-encoded datatypes, + in the Cedille type theory. Cedille is a pure type + theory extending the Curry-style Calculus of + Constructions with implicit products, primitive + heterogeneous equality, and dependent intersections. + All data erase to pure lambda terms, and there is no + built-in notion of datatype. The derivations are + generic in the sense that we derive induction for any + datatype which arises as the least fixed point of a + signature functor. We consider Church-style and + Mendler-style lambda-encodings. Moreover, the + isomorphism of these encodings is proved. Also, we + formalize Lambek's lemma as a consequence of expected + laws of cancellation, reflection, and fusion.}, + url = {http://doi.acm.org/10.1145/3167087%7D, +} + +@proceedings{ICFP06, + address = {Portland, Oregon}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'06}, + month = sep, + title = {International Conference on Functional Programming}, + year = {2006}, +} + +@proceedings{TPHOLs09, + booktitle = {International Conference on Theorem Proving in + Higher-Order Logics}, + key = {TPHOLs09}, + month = aug, + series = {Lecture Notes in Computer Science}, + title = {International Conference on Theorem Proving in + Higher-Order Logics}, + volume = {5674}, + year = {2009}, +} + +@proceedings{POPL14, + booktitle = {Symposium on Principles of Programming Languages}, + key = {POPL'14}, + publisher = {ACM Press}, + title = {Symposium on Principles of Programming Languages}, + year = {2014}, +} + +@proceedings{ICFP16, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'16}, + month = sep, + title = {International Conference on Functional Programming}, + year = {2016}, +} + +@proceedings{ICFP10, + address = {Baltimore, MD}, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'10}, + month = sep, + title = {International Conference on Functional Programming}, + year = {2010}, +} + +@proceedings{WTPP92, + booktitle = {Workshop on Types for Proofs and Programs}, + title = {Workshop on Types for Proofs and Programs}, + year = {1992}, +} + +@proceedings{CPP18, + booktitle = {Certified Programs and Proofs}, + title = {Certified Programs and Proofs}, + year = {2018}, +} + +@proceedings{POPL92, + booktitle = {Symposium on Principles of Programming Languages}, + key = {POPL'92}, + month = jan, + title = {Symposium on Principles of Programming Languages}, + year = {1992}, +} + +@proceedings{TIC97, + booktitle = {International Workshop on Types in Compilation}, + key = {TIC'97}, + month = jun, + title = {International Workshop on Types in Compilation}, + year = {1997}, +} + +@proceedings{LICS89, + booktitle = {Annual Symposium on Logic in Computer Science}, + key = {LICS'89}, + title = {Annual Symposium on Logic in Computer Science}, + year = {1989}, +} + +@proceedings{TLCA93, + booktitle = {International conference on Typed Lambda Calculi and + Applications}, + editor = {M. Bezem and J. Groote}, + key = {TLCA'93}, + month = mar, + publisher = {LNCS 664, Springer-Verlag}, + title = {International conference on Typed Lambda Calculi and + Applications}, + year = {1993}, +} + +@proceedings{ICFP97, + booktitle = {International Conference on Functional Programming}, + key = {ICFP'97}, + month = jun, + publisher = {ACM Press}, + title = {International Conference on Functional Programming}, + year = {1997}, +} + +@proceedings{POPL16, + booktitle = {Symposium on Principles of Programming Languages}, + key = {POPL'16}, + month = jan, + publisher = {ACM Press}, + title = {Symposium on Principles of Programming Languages}, + year = {2016}, +} +

View it on GitLab: https://gitlab.com/monnier/typer/commit/04cd748685a53d8917dda3c6de26c46accbf...