@string{proc = "Proceedings of the\ "} @string{cmu-cs = "Carnegie Mellon University, School of Computer Science"} @string{cornell-cs = "Department of Computer Science, Cornell University"} @string{dec-src = "Digital Equipment Corporation, Systems Research Center"} @string{edin-cs = "Department of Computer Science, University of Edinburgh"} @string{inria = "Institut National de Recherche en Informatique et Automatique (INRIA)"} @string{yale-cs = "Yale University, Department of Computer Science"} %% Conferences @string{cade = "International Conference on Automated Deduction"} @string{csl = "International Workshop on Computer Science Logic"} @string{esop = "European Symposium on Programming"} @string{fool = "Foundations of Object-Oriented Languages Workshop"} @string{fpca = "Conference on Functional Programming Languages and Computer Architecture"} @string{icalp = "International Colloquium on Automata, Languages, and Programming"} @string{icfp = "{ACM SIGPLAN} International Conference on Functional Programming"} @string{lfp = "{ACM} Conference on {Lisp} and Functional Programming"} @string{lics = "{IEEE} Symposium on Logic in Computer Science"} @string{mfps = "Mathematical Foundations of Programming Semantics"} @string{osdi = "Symposium on Operating Systems Design and Implementation"} @string{pldi = "{ACM SIGPLAN} Conference on Programming Language Design and Implementation"} @string{popl = "{ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages"} @string{sosp = "{ACM} Symposium on Operating Systems Principles"} @string{tacs = "Theoretical Aspects of Computer Software"} @string{tlca = "International Conference on Typed Lambda Calculi and Applications"} @string{tldi = "{ACM SIGPLAN} Workshop in Types in Language Design and Implementation"} @string{sigmod = "Proc. {ACM} {SIGMOD} International Conference on Management of Data"} @string{oopsla = "{ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages and Applications"} @string{sigcomm = "Proc. {SIGCOMM} Symposium on Communications Architectures and Protocols"} @string{ieeesp = "IEEE Symposium on Research in Security and Privacy"} @string{rtss = "Real-Time Systems Symposium"} %% Workshops @string{tic = "{ACM} {SIGPLAN} Workshop on Types in Compilation"} @string{wcsss = "{ACM} {SIGPLAN} Workshop on Compiler Support for System Software"} @string{hotos = "Workshop on Hot Topis in Operating Systems"} @string{lctes = "Proceedings of the {ACM} {SIGPLAN} Workshop on Languages, Compilers, and Tools for Embedded Systems"} @string{pepm = "{ACM} {SIGPLAN} Workshop on Partial Evaluation and Semantics-Based Program Manipulation"} @string{hoots = "International Workshop on Higher Order Operational Techniques in Semantics"} %% Journals @string{iandc = "Information and Computation"} @string{jacm = "Journal of the {ACM}"} @string{jfp = "Journal of Functional Programming"} @string{mscs = "Mathematical Structures in Computer Science"} @string{tcs = "Theoretical Computer Science"} @string{toplas = "{ACM} Transactions on Programming Languages and Systems"} @string{tse = "{IEEE} Transactions on Software Engineering"} @String{j-LISP-SYMB-COMPUT = "Lisp and Symbolic Computation"} @string{hosc = "Higher-Order and Symbolic Computation"} @string{lncs = "Lecture Notes in Computer Science"} @string{academic = "Academic Press"} @string{addison = "Addison-Wesley"} @string{cambridge-press = "Cambridge University Press"} @string{chapman = "Chapman \& Hall"} @string{elsevier = "Elsevier"} @string{mit-press = "The MIT Press"} @string{noholland = "North-Holland"} @string{springer = "Springer-Verlag"} @string{sigplan-notices = "{SIGPLAN} Notices"} @string{cam-ma = "Cambridge, Massachusetts"} @string{ith-ny = "Ithaca, New York"} @string{pgh-pa = "Pittsburgh, Pennsylvania"} @string{o1="First "} @string{o2="Second "} @string{o3="Third "} @string{o4="Fourth "} @string{o5="Fifth "} @string{o6="Sixth "} @string{o7="Seventh "} @string{o8="Eighth "} @string{o9="Ninth "} @string{o10="Tenth "} @string{o11="Eleventh "} @string{o12="Twelfth "} @string{o13="Thirteenth "} @string{o14="Fourteenth "} @string{o15="Fifteenth "} @string{o16="Sixteenth "} @string{o17="Seventeenth "} @string{o18="Eighteenth "} @string{o19="Nineteenth "} @string{o20="Twentieth "} @string{o21="Twenty-First "} @string{o22="Twenty-Second "} @string{o23="Twenty-Third "} @string{o24="Twenty-Fourth "} @string{o25="Twenty-Fifth "} @string{o26="Twenty-Sixth "} @string{o27="Twenty-Seventh "} @string{o28="Twenty-Eighth "} @string{o29="Twenty-Ninth "} @string{o30="Thirtieth "} %% Ack for downloaded bib entry @String{ack-nhfb = "Nelson H. F. Beebe, Center for Scientific Computing, University of Utah, Department of Mathematics, 322 INSCC, 155 S 1400 E RM 233, Salt Lake City, UT 84112-0090, USA, Tel: +1 801 581 5254, FAX: +1 801 585 1640, +1 801 581 4148, e-mail: \path|beebe@math.utah.edu|, \path|beebe@acm.org|, \path|beebe@ieee.org| (Internet), URL: \path|http://www.math.utah.edu/~beebe/|"} @inproceedings{deferred-type-errors, author = "Dimitrios Vytiniotis and Simon {Peyton Jones} and Pedro Magalhaes", title = "Equality proofs and deferred type errors", booktitle = {Proceedings of {ACM SIGPLAN} International Conference on Functional Programming (ICFP '12)}, pages = "341-352", year = 2012 } @inproceedings{ductilej, author = "Michael Bayne and Richard Cook and Michael Ernst", title = "Always-available static and dynamic feedback", booktitle = "Proceedings of 33rd International Conference on Software Engineering (ICSE'11)", year = 2011, pages = "521-530", address = "Hawaii" } @INCOLLECTION{pottier:pierce-chapter, AUTHOR = {Fran\c{c}ois Pottier and Didier R{\'{e}}my}, TITLE = {The Essence of {ML} Type Inference}, BOOKTITLE = {Advanced Topics in Types and Programming Languages}, PAGES = {389--489}, PUBLISHER = {MIT Press}, YEAR = {2005}, EDITOR = {Benjamin C. Pierce}, CHAPTER = {10}, html = {http://cristal.inria.fr/attapl/} } @article{gill-hutton:worker-wrapper, author = "Andy Gill and Graham Hutton", title = "The worker/wrapper transformation", journal = {Journal of Functional Programming}, volume = {19}, issue = {2}, page = {227-251}, year = 2009 } @article{pjv:modular, author = {Dimitrios Vytiniotis and Simon {Peyton Jones} and Tom Schrijvers and Martin Sulzmann}, title = "OutsideIn(X): modular type inference with local assumptions", journal = {Journal of Functional Programming}, volume = {21}, issue = {4-5}, page = {333-412}, year = 2011 } @article{rossberg08, author = {Andreas Rossberg}, title = {Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {218}, year = {2008}, pages = {313-336}, bibsource = {DBLP, http://dblp.uni-trier.de} } @InProceedings{mcbride:levitation, author = {James Chapman and Pierre-\'{E}variste Dagand and Conor McBride and Peter Morris}, title = {The Gentle Art of Levitation}, booktitle = {Proceedings of the Fifteenth {ACM SIGPLAN} International Conference on Functional Programming (ICFP '10)}, year = 2010, address = {Baltimore, MD, USA}, month = {September}, note = {To appear.}} # doi = {http://dx.doi.org/10.1016/0890-5401(91)90066-B}, @article{deBruijn:telescopes, author = {de Bruijn, N. G.}, title = {Telescopic mappings in typed lambda calculus}, journal = {Inf. Comput.}, volume = {91}, number = {2}, year = {1991}, issn = {0890-5401}, pages = {189--204}, publisher = {Academic Press, Inc.}, address = {Duluth, MN, USA}, } @inproceedings{johann:gadt, author = {Patricia Johann and Neil Ghani}, title = {Foundations for structured programming with GADTs}, booktitle = {POPL}, year = {2008}, pages = {297-308}, ee = {http://doi.acm.org/10.1145/1328438.1328475}, crossref = {DBLP:conf/popl/2008}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/popl/2008, editor = {George C. Necula and Philip Wadler}, title = {Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008}, booktitle = {POPL}, publisher = {ACM}, year = {2008}, isbn = {978-1-59593-689-9}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{xi:grdt, author = {Hongwei Xi and Chiyan Chen and Gang Chen}, title = {Guarded recursive datatype constructors}, booktitle = {POPL}, year = {2003}, pages = {224-235}, ee = {http://doi.acm.org/10.1145/640128.604150}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{crary:syntactic-recursive, author = {Karl Crary and Robert Harper}, title = {Syntactic Logical Relations for Polymorphic and Recursive Types}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {172}, year = {2007}, pages = {259-299}, note = {Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin}, ee = {http://dx.doi.org/10.1016/j.entcs.2007.02.010}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{ahmed:step-indexed, author = {Amal J. Ahmed}, title = {Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types}, booktitle = {ESOP}, year = {2006}, pages = {69-83}, ee = {http://dx.doi.org/10.1007/11693024_6}, crossref = {DBLP:conf/esop/2006}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Book{kleene:mathematical-logic, author = {Stephen Cole Kleene}, title = {Mathematical Logic}, publisher = {Wiley}, year = 1967 } @inproceedings{Swamy:2009:TTC:1596550.1596598, author = {Swamy, Nikhil and Hicks, Michael and Bierman, Gavin M.}, title = {A theory of typed coercions and its applications}, booktitle = {Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming}, series = {ICFP '09}, year = {2009}, isbn = {978-1-60558-332-7}, location = {Edinburgh, Scotland}, pages = {329--340}, numpages = {12}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {coercion insertion, gradual typing, nonambiguity, provenance, type-directed translation}, } @incollection{Remy-Yakobowski:xmlf, author = {R\'{e}my, Didier and Yakobowski, Boris}, affiliation = {INRIA Paris - Rocquencourt}, title = {A {Church}-Style Intermediate Language for {MLF}}, booktitle = {Functional and Logic Programming}, series = {Lecture Notes in Computer Science}, editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, German}, publisher = {Springer Berlin / Heidelberg}, pages = {24-39}, volume = {6009}, also = {http://gallium.inria.fr/~remy/mlf/}, abstract = {MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System-F explicit first-class polymorphism. We present xMLF, a Church-style version of MLF with full type information that can easily be maintained during reduction. All parameters of functions are explicitly typed and both type abstraction and type instantiation are explicit. However, type instantiation in xMLF is more general than type application in System F. We equip xMLF with a small-step reduction semantics that allows reduction in any context and show that this relation is confluent and type preserving. We also show that both subject reduction and progress hold for weak-reduction strategies, including call-by-value with the value-restriction.}, year = {2010} } @InProceedings{Remy-Yakobowski:mlf-type-inference, AUTHOR = {Didier Remy and Boris Yakobowski}, TITLE = {{E}fficient {T}ype {I}nference for the {MLF} Language: a graphical and constraints-based approach}, BOOKTITLE = {The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08)}, YEAR = 2008, ADDRESS = {Victoria, BC, Canada}, MONTH = Sep, ALSO = {http://gallium.inria.fr/~remy/mlf/}, PDF = {http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski@icfp08:mlf-type-inference.pdf}, pages = {63--74}, doi = {http://doi.acm.org/10.1145/1411203.1411216}, ABSTRACT = { MLF is a type system that seamlessly merges ML-style type inference with System-F polymorphism. We propose a system of graphic (type) constraints that can be used to perform type inference in both ML or MLF. We show that this constraint system is a small extension of the formalism of graphic types, originally introduced to represent MLF types. We give a few semantic preserving transformations on constraints and propose a strategy for applying them to solve constraints. We show that the resulting algorithm has optimal complexity for MLF type inference, and argue that, as for ML, this complexity is linear under reasonable assumptions. } } @inproceedings{xi:cut-elimination, author = "Chiyan Chen and Dengping Zhu and Hongwei Xi", title = {{Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell}}, booktitle = "Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages", publisher = "Springer-Verlag LNCS vol. 3057", year = "2004", month = "June", pages = "239--254", address = "Dallas, TX", abstract = {{ Gentzen's Hauptsatz -- cut elimination theorem -- in sequent calculi reveals a fundamental property on logic connectives in various logics such as classical logic and intuitionistic logic. In this paper, we implement a procedure in Haskell to perform cut elimination for intuitionistic sequent calculus, where we use types to guarantee that the procedure can only return a cut-free proof of the same sequent when given a proof of a sequent that may contain cuts. The contribution of the paper is two-fold. On the one hand, we present an interesting (and somewhat unexpected) application of the current type system of Haskell, illustrating through a concrete example how some typical use of dependent types can be simulated in Haskell. On the other hand, we identify several problematic issues with such a simulation technique and then suggest some approaches to addressing these issues in Haskell. }} } @inproceedings{HList-HW04, author = {Oleg Kiselyov and Ralf L\"{a}mmel and Keean Schupke}, title = "{Strongly typed heterogeneous collections}", booktitle = "{Haskell '04: Proceedings of the ACM SIGPLAN workshop on Haskell}", year = {2004}, isbn = {1-58113-850-4}, pages = {96--107}, location = {Snowbird, Utah, USA}, doi = {http://doi.acm.org/10.1145/1017472.1017488}, publisher = {ACM Press}, } @Unpublished{augustsson:silly, author = {Lennart Augustsson and Kent Petersson}, title = {Silly Type Families}, note = {Available from \url{http://www.cs.pdx.edu/~sheard/papers/silly.pdf}}, month = sep, year = 1994, annote = {GADTs} } @inproceedings{sheard:omega, title = "Meta-programming with built-in type equality", author = "Tim Sheard and Emir Pasalic", booktitle = "Proc 4th International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork", month = jul, year = 2004, pages = "106--124", keywords = "phantom types, type indexed data types" } @TechReport{cheney-hinze:phantom-types, author = {James Cheney and Ralf Hinze}, title = {First-Class Phantom Types}, institution = {Cornell University}, year = 2003, type = {CUCIS}, number = {TR2003-1901} } @InCollection{Remy!records, author = "Didier R\'{e}my", title = "Type Inference for Records in a Natural Extension of {ML}", booktitle = "Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design", publisher = "MIT Press", year = 1993, editor = "Carl A. Gunter and John C. Mitchell" } %% A %% @article{abadi+:dynamic, author = "Mart\'{\i}n Abadi and Luca Cardelli and Benjamin Pierce and Gordon Plotkin", title = "Dynamic typing in a statically-typed language", journal = toplas, year = 1991, volume = 13, number = 2, month = "April", pages = "237--268", } @article{ Abadi92, author = "Mart\'{\i}n Abadi and Luca Cardelli and Benjamin Pierce and Didier R\'{e}my", title = "Dynamic Typing in Polymorphic Languages", journal = "Journal of Functional Programming", volume = "5", number = "1", pages = "111--130", month = jan, annnote = "Summary in \bgroup \em ACM SIGPLAN Workshop on ML and its Applications\egroup, June 1992", year = 1995, bcp = yes } @article{abadi+:explicit-subs, author = "Mart\'{\i}n Abadi and Luca Cardelli and Pierre-Louis Curien and Jean-Jacques L\'{e}vy", title = "Explicit Substitutions", journal = jfp, year = 1991, volume = 1, number = 4, pages = "375--416", } @inproceedings{abadi+:object-interp, author = "Mart\'{\i}n Abadi and Luca Cardelli and Ramesh Viswanathan", title = "An Interpretation of Objects and Object Types", booktitle = o23 # " " # popl, year = 1996, month = jan, address = "St.\ Petersburg, Florida", pages = "296--409", } @inproceedings{abadi+:prim-objects, author = "Mart\'{\i}n Abadi and Luca Cardelli", title = "A Theory of Primitive Objects: Untyped and First-Order Systems", booktitle = tacs, year = 1994, month = apr, pages = "296--320", series = lncs, volume = 789, publisher = springer, } @book{abadi+:thy-objects, author = "Mart\'{\i}n Abadi and Luca Cardelli", title = "A Theory of Objects", publisher = springer, year = 1996, } @inproceedings{abadi:protection-in-trans, author = "Mart\'{\i}n Abadi", title = "Protection in Programming-Language Translations", booktitle = o25 # " " # icalp, month = jul, year = 1998, } @InProceedings{abadi+:dcc, author = {Mart\'{\i}n Abadi and Anindya Banerjee and Nevin Heintze and Jon G. Riecke}, title = {A Core Calculus of Dependency}, booktitle = o26 # " " # popl, pages = {147--160}, year = 1999, address = {San Antonio, Texas}, month = jan } @inproceedings{aczel:frege-revisit, author = "Peter Aczel", title = "{F}rege Structures Revisited", booktitle = "Proceedings of the 1983 Marstrand Workshop", editor = "B. {Nordstr\"{o}m} and J. Smith", year = 1983, } @manual{ada:manual, key = {ISOA}, edition = {6.0}, month = dec, organization = {International Organisation for Standardisation and International Electrotechnical Commission}, title = {International Standard ISO/IEC 8652:1995 Ada Reference Manual: Language and Standard Libraries }, year = 1994, url = "http://www.adahome.com/rm95/" } @Manual{c:standard, title = {ISO/IEC 9899:1999 Programming Languages--{C}}, key = {ISOC}, organization = {International Organisation for Standardization and International Electrotechnical Commission}, month = dec, year = 1999 } @Manual{c++:standard, title = {ISO/IEC 14882:1998 Information Technology--Programming Languages--{C++}}, key = {ISOCP}, organization = {International Organisation for Standardization and International Electrotechnical Commission}, month = sep, year = 1998 } @inproceedings{aditya+:gc, author = "Shail Aditya and Christine Flood and James Hicks", title = "Garbage Collection for Strongly-Typed Languages using Run-Time Type Reconstruction", booktitle = 1994 # " " # lfp, month = jun, pages = "12--23", year = 1994, address = "Orlando" } @inproceedings{ agesen97adding, author = "Ole Agesen and Stephen N. Freund and John C. Mitchell", title = "Adding Type Parameterization to the {Java} Language", booktitle = "{ACM} {S}ymposium on {O}bject {O}riented {P}rogramming: {S}ystems, {L}anguages, and {A}pplications ({OOPSLA})", address = "Atlanta, GA", pages = "49--65", year = "1997", url = "citeseer.nj.nec.com/agesen97adding.html" } @inproceedings{aiken+:type-inclusion, author = "Alexander Aiken and Edward L. Wimmers", title = "Type Inclusion Constraints and Type Inference", booktitle = "FPCA93: " # fpca, year = 1993, pages = "31--41", } @inproceedings{allen+:reflection, author = "Stuart F. Allen and Robert L. Constable and Douglas J. Howe and William E. Aitken", title = "The Semantics of Reflected Proof", booktitle = o5 # " " # lics, year = 1990, month = jun, pages = {95--105}, address = {Philadelphia, Pennsylvania}, publisher = {IEEE Computer Society Press} } @phdthesis{allen:phd, author = "Stuart Allen", title = "A Non-Type-Theoretic Semantics for Type-Theoretic Language", school = cornell-cs, year = 1987, address = ith-ny, } @inproceedings{allen:tt-semant, author = "Stuart Allen", title = "A Non-Type-Theoretic Definition of {Martin-L\"{o}f}'s Types", booktitle = o2 # " " # lics, year = 1987, month = jun, pages = "215--221", address = ith-ny, } @article{amadio+:subtyping-rectypes, author = "Roberto Amadio and Luca Cardelli", title = "Subtyping Recursive Types", journal = toplas, year = 1993, volume = 15, number = 4, pages = "575--631", } @inproceedings{appel+:cont-close, author = "Andrew W. Appel and Trevor Jim", title = "Continuation-Passing, Closure-Passing Style", bookTitle = o16 # " " # popl, year = 1989, month = jan, pages = "293--302", address = "Austin", } @inproceedings{appel+:smlnj, title = "{S}tandard {ML} of {N}ew {J}ersey", author = "Andrew W. Appel and David B. MacQueen", booktitle = "Third International Symposium on Programming Language Implementation and Logic Programming", publisher = springer, month = aug, year = "1991", pages = "1--13", volume = 528, series = lncs, } @book{appel:cont-compiling, author = "Andrew W. Appel", title = "Compiling with Continuations", publisher = cambridge-press, year = 1992, } @inproceedings{appel+:pcc, author = {Andrew W. Appel and Amy P. Felty}, title = {A Semantic Model of Types and Machine Instructions for Proof-Carrying Code}, booktitle = o27 # " " # popl, month = jan, year = 2000, address = "Boston", pages = "243--253" } @inproceedings{ armstrong97development, author = "Joe Armstrong", title = "The development of {Erlang}", booktitle = "Proceedings of the {ACM} {SIGPLAN} International Conference on Functional Programming ({ICFP} '97)", pages = "196--203", year = "1997", url = "citeseer.nj.nec.com/37831.html" } @inproceedings{aspinall:subtype-singleton, author = "David Aspinall", title = "Subtyping with Singleton Types", booktitle = o8 # " " # csl, year = 1994, month = sep, address = "Kazimierz, Poland", series = lncs, volume = 933, publisher = springer, pages = "1--15", } @inproceedings{audebaud:partial-coq, title = "Partial Objects in the Calculus of Constructions", author = "Philippe Audebaud", booktitle = o6 # " " # lics, year = 1991, month = jul, pages = "86--95", address = "Amsterdam", } @InProceedings{augustsson:cayenne, author = {Lennart Augustsson}, title = {Cayenne--a language with dependent types}, booktitle = o3 # " " # icfp, pages = {239--250}, year = 1998, month = sep, } %% B %% @Article{barendregt:impact, author = {Henk P. Barendregt}, title = { The impact of the lambda calculus }, journal = {Bulletin of Symbolic Logic}, year = 1997, volume = 3, number = 2 } @InCollection{barendregt:pts, author = {Henk P. Barendregt }, editor = {Samson Abramsky and Dov M. Gabbay and Thomas S. E. Maibaum}, booktitle = {Handbook of Logic in Computer Science}, title = {Lambda Calculi with Types}, publisher = {Clarendon Press}, year = 1992, volume = 2, pages = {117--309}, address = {Oxford} } @Book{barendregt:book, author = {Hendrik P. Barendregt}, title = {The Lambda Calculus, its Syntax and Semantics}, publisher = {North Holland}, year = 1984, edition = {Second} } @inproceedings{basin:automated-partial-fns, author = "David A. Basin", title = "An Environment for Automated Reasoning about Partial Functions", booktitle = o9 # " " # cade, series = lncs, volume = 310, publisher = springer, year = 1988, } @article{bates+:proofs-as-programs, author = "Joseph L. Bates and Robert L. Constable", title = "Proofs as Programs", journal = toplas, year = 1985, volume = 7, number = 1, pages = "113--136", month = jan, } @phdthesis{bates:phd, author = "Joseph L. Bates", title = "A Logic for Correct Program Development", year = 1979, school = cornell-cs, address = ith-ny, } @article{beeson:recursive-models, author = "Michael Beeson", title = "Recursive Models for Constructive Set Theories", journal = "Annals of Mathematical Logic", volume = 23, pages = "127--178", year = 1982, } @InProceedings{berger91nbe, author = {Ulrich Berger and Helmut Schwichtenberg}, title = {An inverse of the evaluation functional for typed $lambda$-calculus}, booktitle = { Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science}, pages = {203--211}, year = {1991 }, editor = { R. Vemuri}, address = {Los Alamitos}, publisher = {IEEE Computer Society Press} } @inproceedings{benton+:sml-to-jvm, author = "Nick Benton and Andrew Kennedy and George Russell", title = "Compiling {Standard} {ML} to {Java} Bytecodes", booktitle = 1998 # " " # icfp, year = 1998, month = sep, address = "Baltimore", pages = "129--140", } @inproceedings{bershad+:spin, title = "Extensibility, Safety and Performance in the {SPIN} Operating System", author = "Brain Bershad and Stefan Savage and Przemyslaw Pardyak and Emin Sirer and Marc Fiuczynski and David Becker and Craig Chambers and Susan Eggers", booktitle = o15 # " " # sosp, year = 1995, month = dec, pages = "267--284", address = "{C}opper {M}ountain", } @Article{bird+:debruijn, author = {Richard S. Bird and Ross Paterson}, title = {De {B}ruijn Notation as a Nested Datatype}, journal = jfp, year = 1999, volume = 9, number = 1, pages = "77--91", } @InProceedings{bird+:nested, author = {Richard Bird and Lambert Meertens}, title = {Nested Datatypes}, booktitle = "Proceedings 4th Int.\ Conf.\ on Mathematics of Program Construction, {MPC}'98, Marstrand, Sweden, 15--17 June 1998", year = 1998, volume = 1422, series = lncs, pages = "52--67" } @article{ bird99generalised, author = "Richard Bird and Ross Paterson", title = "Generalised Folds for Nested Datatypes", journal = "Formal Aspects of Computing", volume = "11", number = "2", pages = "200--222", year = "1999", editor = "Johan Juering", url = "citeseer.nj.nec.com/bird99generalised.html" } @techreport{birkedal+:kit, title = "The {ML} {K}it (Version 1)", author = "Lars Birkedal and Nick Rothwell and Mads Tofte and David N. Turner", year = "1993", institution = "{D}epartment of {C}omputer {S}cience, {U}niversity of {C}openhagen", number = "93/14" } @inproceedings{birkedal+:rec-type-interp, author = "Lars Birkedal and Robert Harper", title = "Relational Interpretations of Recursive Types in an Operational Setting", pages = "458-490", booktitle = tacs, year = 1997 } @inproceedings{birkedal+:regions, title = "From Region Inference to {v}on {N}eumann Machines via Region Representation Inference", author = "Lars Birkedal and Mads Tofte and Magnus Vejlstrup", booktitle = o23 # " " # popl, year = "1996", month = jan, pages = "171--183", address = "St.\ Petersburg, Florida" } @phdthesis{blume:phd, author = "Matthias Blume", title = "Hierarchical Modularity and Intermodule Optimization", month = nov, year = 1997, school = "Princeton University, Department of Computer Science", address = "Princeton, New Jersey", } @article{boehm+:gc, author = "Hans-J. Boehm and Mark Weiser", title = "Garbage Collection in an uncooperative environment", journal = "Software Practice and Experience", volume = 18, number = 9, year = 1988, month = sep, pages = "807--820", } @inproceedings{boehm:infer-undecidable, author = "Hans-J. Boehm", title = "Partial Polymorphic Type Inference is Undecidable", booktitle = o26 # " Annual Symposium on Foundations of Computer Science", year = 1985, month = oct, pages = "339--345", } @Article{bohm+:algebras, author = {Corrado B\"ohm and Allessandro Berarducci}, title = {Automatic synthesis of typed {$\Lambda$}-programs on term algebras}, journal = tcs, year = 1985, volume = 39, pages = {135-154} } @inproceedings{ bracha98making, author = "Gilad Bracha and Martin Odersky and David Stoutamire and Philip Wadler", title = "Making the Future Safe for the Past: Adding Genericity to the {Java} Programming Language", booktitle = "Object Oriented Programming: Systems, Languages, and Applications ({OOPSLA})", address = "Vancouver, BC", editor = "Craig Chambers", pages = "183--200", year = "1998", url = "citeseer.nj.nec.com/bracha98making.html" } @inproceedings{ bracha93strongtalk, author = "Gibblad Bracha and David Griswold", title = "{Strongtalk: Typechecking Smalltalk in a Production Environment}", booktitle = "Proceedings of the \mbox{OOPSLA}~'93 Conference on Object-oriented Programming Systems, Languages and Applications", pages = "215--230", year = "1993", url = "citeseer.nj.nec.com/bracha93strongtalk.html" } @inproceedings{ brandt97coinductive, author = "Michael Brandt and Fritz Henglein", title = "Coinductive axiomatization of recursive type equality and subtyping", booktitle = "Proc.\ 3d Int'l Conf. on Typed Lambda Calculi and Applications ({TLCA}), Nancy, France, April 2-4, 1997", volume = "1210", publisher = "Springer-Verlag", editor = "Roger Hindley", pages = "63--81", year = "1997", url = "citeseer.nj.nec.com/brandt98coinductive.html" } @inproceedings{breazu-tannen+:computing-w-coercions, author = "Val Breazu-Tannen and Carl A. Gunter and Andre Scedrov", title = "Computing with Coercions", booktitle = 1990 # " " # lfp, year = 1990, pages = "44--60", } @article{breazu-tannen+:implicit-coercion, author = "Val Breazu-Tannen and Thierry Coquand and Carl A. Gunter and Andre Scedrov", title = "Inheritance as Implicit Coercion", journal = iandc, year = 1991, volume = 93, pages = "172--221", } @Article{Bobrow:1988:CLOa, author = "Daniel G. Bobrow and Linda G. Demichiel and Richard P. Gabriel and Sonya E. Keene and Gregor Kiczales And David A. Moon", title = "{Common Lisp Object System} Specification 1. Programmer Interface Concepts", journal = j-LISP-SYMB-COMPUT, volume = "1", number = "2", pages = "245--298", month = sep, year = "1988", CODEN = "LSCOEX", ISSN = "0892-4635", bibdate = "Fri Feb 12 06:09:25 1999", acknowledgement = ack-nhfb, } @Article{Bobrow:1988:CLOb, author = "Daniel G. Bobrow and Linda G. Demichiel and Richard P. Gabriel and Sonya E. Keene and Gregor Kiczales And David A. Moon", title = "{Common Lisp Object System} Specification 2. Functions in the Programmer Interface", journal = j-LISP-SYMB-COMPUT, volume = "1", number = "2", pages = "299--394", month = sep, year = "1988", CODEN = "LSCOEX", ISSN = "0892-4635", bibdate = "Fri Feb 12 06:09:25 1999", acknowledgement = ack-nhfb, } @article{bruce+:binary-methods, author = "Kim B. Bruce and Luca Cardelli and Giuseppe Castagna and The Hopkins Objects Group and Gary T. Leavens and Benjamin C. Pierce", title = "On Binary Methods", journal = "Theory and Practice of Object Systems", volume = 1, number = 3, pages = "221--242", year = 1996, } @inproceedings{bruce+:comp-obj-encodings, author = "Kim B. Bruce and Luca Cardelli and Benjamin C. Pierce", title = "Comparing Object Encodings", booktitle = "Theoretical Aspects of Computer Software", address = "Sendai, Japan", year = 1997, month = sep, } @article{bruce+:modest-model, author = "Kim B. Bruce and Giuseppe Longo", title = "A Modest Model of Records, Inheritance, and Bounded Quantification", journal = iandc, year = 1991, volume = 87, pages = "196--240", } @article{bruce:paradigm-oop, author = "Kim B. Bruce", title = "A Paradigmatic Object-Oriented Programming Language: Design, Static Typing and Semantics", journal = jfp, year = 1994, month = apr, volume = 4, number = 2, pages = "127--206", } %% C %% @inproceedings{canning+:f-bound-oop, author = "Peter Canning and William Cook and Walter Hill and John Mitchell and Walter Olthoff", title = "F-Bounded Quantification for Object-Oriented Programming", booktitle = "FPCA89: " # fpca, year = 1989, month = sep, pages = "273--280", } @inproceedings{cardelli+:fsub, author = "Luca Cardelli and Simone Martini and John C. Mitchell and Andre Scedrov", title = "An Extension of System {F} With Subtyping", booktitle = tacs # " 1991", address = "Sendai, Japan", year = 1991, pages = "750--770", series = lncs, volume = 526, publisher = springer, } @article{cardelli+:fun, author = "Luca Cardelli and Peter Wegner", title = "On Understanding Types, Data Abstraction, and Polymorphism", journal = "Computing Surveys", volume = 17, number = 4, year = 1985, month = dec, pages = "471--522", } @techreport{cardelli+:modula3, title = "Modula-3 Report (Revised)", author = "Luca Cardelli and James Donahue and Lucille Glassman and Mick Jordan and Bill Kalsow and Greg Nelson", month = nov, year = 1989, number = 52, institution = dec-src, } @incollection{cardelli:amber, author = "Luca Cardelli", title = "Amber", booktitle = "Combinators and Functional Programming Languages", publisher = springer, editor = "Guy Coisineau and Pierre-Louis Curien and Bernard Robinet", series = lncs, volume = 242, pages = "48--70", year = 1986 } @techreport{cardelli:extensible-records, author = "Luca Cardelli", title = "Extensible Records in a Pure Calculus of Subtyping", institution = dec-src, year = 1993, type = "SRC Research Report", number = "81", month = jan, } @unpublished{cardelli:f-omega-sub, author = "Luca Cardelli", title = "Notes about {F$^\omega_{<:}$}", note = "Unpublished manuscript", year = 1990, } @techreport{cardelli:fsub-impl, author = "Luca Cardelli", title = "An Implementation of ${F}_{<:}$", institution = dec-src, year = 1993, month = feb, type = "SRC Research Report", number = "97", } @article{cardelli:inherit-semantics, author = "Luca Cardelli", title = "A semantics of multiple inheritance", journal = iandc, volume = 76, pages = "138--164", year = 1988, } @unpublished{cardelli:phase, author = "Luca Cardelli", title = "Phase Distinctions in Type Theory", note = "Unpublished manuscript", year = 1988, month = jan, } @inproceedings{cardelli:power-type, author = "Luca Cardelli", title = "Structural Subtyping and the Notion of Power Type", booktitle = o15 # " " # popl, year = 1988, month = jan, pages = "70--79", address = "San Diego", } @incollection{cardelli:typeful, author = "Luca Cardelli", title = "Typeful Programming", booktitle = "Formal Description of Programming Concepts", year = 1991, publisher = "Springer-Verlag", } @inproceedings{ cartwright98compatible, author = "Robert Cartwright and Guy L. {Steele, Jr.}", title = "Compatible Genericity with Run-time Types for the {Java} Programming Language", booktitle = "{ACM} {S}ymposium on {O}bject {O}riented {P}rogramming: {S}ystems, {L}anguages, and {A}pplications ({OOPSLA}), Vancouver, British Columbia", publisher = "ACM", editor = "Craig Chambers", pages = "201--215", year = "1998", url = "citeseer.nj.nec.com/cartwright98compatible.html" } @Manual{mlton, title = {MLton User Guide}, author = {Henry Cejtin and Matthew Fluet and Suresh Jagannathan and Stephen Weeks}, month = apr, year = 2000, note = {\url{http://www.mlton.org/HTML/main.html}} } @Misc{cert:denial, key = {CERT00}, author = {CERT Coordination Center and the Federal Computer Incident Response Capability (FedCIRC)}, title = {{CERT} Advisory CA-2000-01 Denial-of-Service Developments}, howpublished = {http://www.cert.org/advisories/CA-2000-01.html}, month = jan, year = 2000 } @inproceedings{ chak-keller:more-types, author = {Manuel M. T. Chakravarty and Gabriele Keller}, title = {More Types for Nested Data Parallel Programming}, editor = {Philip Wadler}, booktitle = {Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00)}, year = 2000, publisher = {ACM Press}, pages = {94--105}, url = {citeseer.nj.nec.com/chakravarty00more.html} } @InProceedings{chak:array-fusion, author = {Manuel M. T. Chakravarty and Gabriele Keller}, title = {Functional Array Fusion}, booktitle = {Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming}, pages = {205--216}, year = 2002, address = {Florence, Italy}, month = sep, publisher = {{ACM} Press} } @InProceedings{cheung+:routing, author = {Steven Cheung and Karl N. Levitt}, title = {Protecting routing infrastructures from denial of service using cooperative intrusion detection }, booktitle = {Proceedings of the Workshop on New Paradigms}, year = 1998, address = {Charlottesville, VA}, month = sep } @InProceedings{chin00sized, author = {Wei-Ngan Chin and Siau-Cheng Khoo}, title = {Calculating Sized Types}, booktitle = pepm, pages = "62--72", year = 2000, address = {Boston,USA}, month = jan } @Article{church:simple-types, author = {Alonzo Church}, title = {A Formulation of the Simple Theory of Types}, journal = {Journal of Symbolic Logic}, year = 1940, volume = 5, pages = {56--68} } @InProceedings{clark90:_archit_consid, author = {D. Clark and D. Tennenhouse}, title = {Architectural Considerations for a new generation of protocols}, booktitle = sigcomm, year = 1990, address = {Philadelphia, Pennsylvania}, month = sep } @TechReport{generic-haskell, author = {Dave Clarke and Ralf Hinze and Johan Jeuring and Andres L\"{o}h and Jan de Wit}, title = {The {G}eneric {H}askell user's guide}, institution = {Utrecht University }, year = 2001, number = {UU-CS-2001-26} } @techreport{CoFu92, author = "Robin Cockett and Tom Fukushima", title = "About {C}harity", institution = "Department of Computer Science, The University of Calgary", month = jun, year = 1992, type = "Yellow Series Report", number = "No.\ 92/480/18" } @InProceedings{cointe:meta-classes, author = {Pierre Cointe}, title = {Metaclasses are first class: The {ObjVlisp} model}, booktitle = {Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)}, pages = {156--167}, year = 1987, address = { Orlando, FL} } @MISC{COM, KEY = {COM}, TITLE = {{M}icrosoft {COM} Technologies}, month = jan, year = 2002, NOTE = {\url{http://www.microsoft.com/com/default.asp}} } @article{compagnoni+:intersect-mult-inherit, author = "Adriana B. Compagnoni and Benjamin C. Pierce", title = "Higher-Order Intersection Types and Multiple Inheritance", journal = mscs, pages = "469--501", month = oct, year = 1996, volume = 6, number = 5, } @inproceedings{constable+:comp-founds-fn-thy, author = "Robert L. Constable and Scott Fraser Smith", title = "Computational Foundations of Basic Recursive Function Theory", booktitle = o3 # " " # lics, year = 1988, address = "Edinburgh, Scotland", pages = "360--371", month = jul, } @inproceedings{constable+:intensional-analysis, author = "Robert L. Constable and Karl Crary", title = "Computational Complexity and Induction for Partial Computable Functions in Type Theory", booktitle = "Feferman Festschrift", year = 1998, month = dec } @book{constable+:nuprl, title = "Implementing Mathematics with the {N}uprl Proof Development System", author = "Robert L. Constable and Stuart F. Allen and H. Mark Bromley and W. Rance Cleaveland and James F. Cremer and Robert W. Harper and Douglas J. Howe and Todd B. Knoblock and Nax Paul Mendler and Prakash Panangaden and James T. Sasaki and Scott F. Smith", publisher = "Prentice-Hall", year = 1986, } @inproceedings{constable+:partial-objs, author = "Robert L. Constable and Scott F. Smith", title = "Partial Objects in Constructive Type Theory", booktitle = o2 # " " # lics, year = 1987, month = jun, pages = "183--193", address = ith-ny, } @article{constable+:plcv3, author = "Robert L. Constable and Daniel R. Zlatin", title = "The Type Theory of {PL/CV3}", journal = toplas, volume = 6, number = 1, year = 1984, month = jan, pages = "94--117", } @techreport{constable:ita, author = "Robert L. Constable", title = "Intensional Analysis of Functions and Types", year = 1982, month = jun, number = "CSR-118-82", institution = edin-cs, } @incollection{constable:math-as-programming-logic, author = "Robert L. Constable", title = "Constructive Mathematics as a Programming Logic {I}: Some Principles of Theory", booktitle = "Topics in the Theory of Computation", series = "Annals of Discrete Mathematics", volume = 24, publisher = elsevier, year = 1985, pages = "21--37", note = "Selected papers of the International Conference on Foundations of Computation Theory 1983", } @inproceedings{constable:tt-found-cs, author = "Robert L. Constable", title = "Type Theory as a Foundation for Computer Science", booktitle = tacs # " 1991", address = "Sendai, Japan", year = 1991, pages = "226--243", series = lncs, volume = 526, publisher = springer, } @incollection{constable:types-logic-math-prog, author = "Robert L. Constable", title = "Types in Logic, Mathematics and Programming", booktitle = "Handbook of Proof Theory", editor = "Sam Buss", chapter = 10, year = 1998, publisher = "Elsevier Science", } @inproceedings{cook+:inherit-not-subtyping, author = "William R. Cook and Walter L. Hill and Peter S. Canning", title = "Inheritance is not Subtyping", booktitle = o17 # " " # popl, pages = "125--135", month = jan, year = 1990, address = "San Francisco", } @TechReport{coq-manual, title = "The {Coq} Proof Assistant Reference Manual: Version 6.1", author = "Bruno Barras and Samuel Boutin and Cristina Cornes and {Judica\"{e}l} Courant and Jean-Christophe Filli\^{a}tre and Eduardo Gim\'{e}nez and Hugo Herbelin and G\'{e}rard Huet and C\'{e}sar {Mu\~{n}oz} and Chetan Murthy and Catherine Parent and Christine Paulin-Mohring and Amokrane {Sa\"{\i}bi} and Benjamin Werner", institution = "{INRIA-Rocquencourt, CNRS and ENS Lyon}", number = "RT-0203", year = "1997", } @article{coquand+:coc, author = "Thierry Coquand and G\'{e}rard Huet", title = "The Calculus of Constructions", journal = iandc, year = 1988, volume = 76, pages = "95--120", } @inproceedings{coquand:girard-paradox, author = "Thierry Coquand", title = "An Analysis of {G}irard's Paradox", booktitle = o1 # " " # lics, year = 1986, month = jun, pages = "227--236", address = cam-ma, } @incollection{coquand:investigate-coc, author = "Thierry Coquand", title = "Metamathematical Investigations of a Calculus of Constructions", booktitle = "Logic and Computer Science", pages = "91--122", year = 1990, series = "The {APIC} Series", volume = 31, editor = "P. Odifreddi", publisher = academic, } @InProceedings{coquand+:inductively, author = {Thierry Coquand and Christin Paulin-Mohring}, title = {Inductively Defined Types}, booktitle = {COLOG-88 International Conference on Computer Logic}, pages = {50--66}, year = 1988, editor = {P. Martin-L\"{o}f and G. Mints}, volume = 417, series = lncs, address = {Tallinn, USSR}, month = dec, publisher = springer } @Incollection{coquand:new-paradox, author = {Thierry Coquand}, editor = {Dag Prawitz and Brian Skyrms and Dag Westerst\aa{}hl}, booktitle = {Logic, Methodology and Philosophy of Science IX : Proceedings of the Ninth International Congress of Logic, Methodology, and Philosophy of Science, Uppsala, Sweden, August 7-14, 1991}, title = {A New Paradox in Type Theory}, publisher = elsevier, volume = 134, year = 1994, pages = "555--570", address = {Amsterdam}, url = "citeseer.nj.nec.com/coquand94new.html" } @InProceedings{coquand:conversion, author = {Thierry Coquand}, editor = {G\'{e}rard Huet and Gordon Plotkin}, booktitle = {Logical Frameworks}, title = {An Algorithm for Testing Conversion in Type Theory}, publisher = cambridge-press, year = 1991, pages = {255-277} } @inproceedings{crary+:capabilities, author = "Karl Crary and David Walker and Greg Morrisett", title = "Typed Memory Management in a Calculus of Capabilities", year = 1999, month = jan, booktitle = o26 # " " # popl, address = "San Antonio, Texas", } @techreport{crary+:datatypes, author = "Karl Crary and Robert Harper and Perry Cheng and Leaf Petersen and Chris Stone", title = "Transparent and Opaque Interpretations of Datatypes", institution = cmu-cs, month = nov, year = 1998, number = "CMU-CS-98-177", memo = "Also published as Fox Memorandum CMU-CS-FOX-98-04.", } @techreport{crary+:lx-tr, author = "Karl Crary and Stephanie Weirich", title = "Flexible Type Analysis (Extended version)", year = 1999, institution = cornell-cs, } @InProceedings{crary+:popcron, author = {Karl Crary and Stephanie Weirich}, title = {Resource Bound Certification}, booktitle = o27 # " " # popl, pages = {184--198}, year = 2000, address = "Boston, MA", month = jan } @inproceedings{crary+:recmod, author = "Karl Crary and Robert Harper and Sidd Puri", title = "What is a Recursive Module?", booktitle = 1999 # " " # pldi, month = may, year = 1999, address = "Atlanta", memo = "Also published as TR CMU-CS-98-168 and Fox Memorandum CMU-CS-FOX-98-03.", } @inproceedings{crary:admissibility, author = "Karl Crary", title = "Admissibility of Fixpoint Induction over Partial Types", booktitle = o15 # " " # cade, year = 1998, month = jul, address = "Lindau, Germany", pages = "270--285", publisher = springer, series = lncs, volume = 1421, note = "Extended version published as CMU technical report CMU-CS-98-164." } @techreport{crary:admissibility-tr, author = "Karl Crary", title = "Admissibility of Fixpoint Induction over Partial Types", institution = cmu-cs, year = 1998, month = oct, number = "CMU-CS-98-164", } @inproceedings{crary:ho-subtyping-impl, author = "Karl Crary", title = "Foundations for the Implementation of Higher-Order Subtyping", booktitle = 1997 # " " # icfp, year = 1997, month = jun, address = "Amsterdam", pages = "125--135", } @manual{crary:kml96-manual, title = "{KML} Reference Manual", author = "Karl Crary", year = 1996, organization = cornell-cs, } @techreport{crary:orei, author = "Karl Crary", title = "Simple, Efficient Object Encoding using Intersection Types", institution = cmu-cs, year = 1999, month = jan, number = "CMU-CS-99-100", memo = "Also published as Fox Memorandum CMU-CS-FOX-99-01", } @techreport{crary:orei-old, author = "Karl Crary", title = "Simple, Efficient Object Encoding using Intersection Types", institution = cornell-cs, year = 1998, month = apr, number = "TR98-1675", } @inproceedings{crary:param-sing, author = "Karl Crary", title = "A Simple Proof Technique for Certain Parametricity Results", booktitle = 1999 # " " # icfp, year = 1999, month = sep, address = "Paris", pages = "82--89", memo = "Also published as CMU-CS-98-185 and Fox Memorandum CMU-CS-FOX-98-06.", } @phdthesis{crary:phd, author = "Karl Crary", title = "Type-Theoretic Methodology for Practical Programming Languages", month = aug, year = 1998, school = cornell-cs, address = ith-ny, } @inproceedings{crary:tt-semant, author = "Karl Crary", title = "Programming Language Semantics in Foundational Type Theory", booktitle = "International Conference on Programming Concepts and Methods", year = 1998, address = "Shelter Island, New York", publisher = chapman, note = "Extended version published as Cornell University technical report TR98-1666.", } @techreport{crary:tt-semant-tr, author = "Karl Crary", title = "Programming Language Semantics in Foundational Type Theory", institution = cornell-cs, year = 1998, month = feb, number = "TR98-1666", address = ith-ny } @InProceedings{crary:subtyping, author = {Karl Crary}, title = {Typed Compilation of Inclusive Subtyping}, booktitle = {International Conference on Functional Programming (ICFP '00)}, year = 2000, address = {Montreal, CA}, month = sep } @inproceedings{curien+:coherence, author = "Pierre-Louis Curien and Giorgio Ghelli", title = "Coherence of Subsumption", booktitle = "Fifteenth Colloquium on Trees in Algebra and Programming", publisher = springer, series = lncs, volume = 431, year = 1990, pages = "132--146", } @article{curien+:confluent-subs, author = "Pierre-Louis Curien and Th\'{e}r\`{e}se Hardin and Jean-Jacques L\'{e}vy", title = "Confluence Properties of Weak and Strong Calculi of Explicit Substitutions", journal = jacm, month = mar, year = 1996, volume = 43, number = 2, pages = "362--397", } @Book{curry-feys, author = {Haskell Curry and Robert Feys}, title = { Combinatory Logic I}, publisher = { North-Holland}, year = 1958 } @inproceedings{czajkowki98:_jres, author = {Grzegorz Czajkowki and Thorsten von Eiken}, title = {{JR}es: A Resource Accounting Interface for Java}, booktitle = "Proceedings of the 1998 " # oopsla, pages = "21--35", year = 1998, volume = 33, number = 10, series = {SIGPLAN Notices}, month = oct } @inproceedings{czajkowski99database, author = {Grzegorz Czajkowski and Tobias Mayr and Praveen Seshadri and Thorsten von Eicken}, title = {Resource Control for Database Extensions}, year = 1999, booktitle = o5 # " " # "USENIX Conference on Object-Oriented Technologies and Systems", month = may, address = {San Diego, California, USA} } %% D %% @article{danvy+:control, author = "Olivier Danvy and Andrzej Filinski", title = "Representing control: a study of the {CPS} transformation", journal = "Mathematical Structures in Computer Science", volume = 2, number = 4, month = dec, year = 1992, pages = "361--391", } @inproceedings{ danvy96typedirected, author = "Olivier Danvy", title = "Type-Directed Partial Evaluation", booktitle = "{POPL}'96: The 23rd {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages, St. Petersburg, Florida, January 1996", pages = "242--257", year = "1996", url = "citeseer.nj.nec.com/danvy96typedirected.html" } @inproceedings{davies+:modal-logic-comp, author = "Rowan Davies and Frank Pfenning", title = "A Modal Analysis of Staged Computation", booktitle = o23 # " " # popl, year = 1996, month = jan, pages = "258--270", } @Article{pfenning+:judgmental-reconstruct, author = {Frank Pfenning and Rowan Davies.}, title = {A Judgmental Reconstruction of Modal Logic}, journal = {Mathematical Structures in Computer Science}, year = 2001, volume = 11, number = 4, pages = {511--540}, month = aug } @inproceedings{davies:temporal-logic-comp, author = "Rowan Davies", title = "A Temporal-Logic Approach to Binding-Time Analysis", booktitle = o11 # " " # lics, year = 1996, month = jul, pages = "184--195", } @incollection{debruijn:automath-survey, author = "Nicolaas Govert de Bruijn", title = "A Survey of the Project {Automath}", booktitle = "To {H.B.} {Curry}: Essays on Combinatory Logic, Lambda-Calculus and Formalism", editor = "J. Roger Seldin and Jonathan R. Hindley", pages = "579--606", publisher = "Academic Press", year = 1980, } @article{debruijn:dummies, author = "Nicolaas Govert de Bruijn", title = "Lambda-Calculus Notation with Nameless Dummies: a Tool for Automatic Formula Manipulation with Application to the {Church-Rosser} Theorem", journal = "Indagationes Mathematicae", volume = 34, number = 5, year = 1972, pages = "381--392", } @Book{des-rivieres:MOP, author = {Gregor Kiczales and Jim des Rivieres and Daniel Bobrow}, title = {The Art of the Meta-Object Protocol}, publisher = mit-press, year = 1991 } @InProceedings{des-rivieres+:implementation-reflective, author = {Jim des Rivieres and Brian Cantwell Smith}, title = {The implementation of procedurally reflective languages}, booktitle = {Conference Record of the 1984 ACM Symposium on LISP and Functional Programming}, pages = {331--347}, year = 1984, address = {Austin, Texas}, publisher = "ACM Press" } @inproceedings{demers+:reflection-survey, author = {Francois-Nicola Demers and Jacques Malenfant}, title = {Reflection and logic, functional and object-oriented programming: a Short Comparative Study}, booktitle = {{IJCAI '95} Workshop on Reflection and Metalevel Architectures and their Applications in AI}, pages = {29--38}, year = 1995, month = aug, url = {citeseer.nj.nec.com/106401.html} } @Article{despeyroux+:functional, author = {{Jo\"{e}lle} Despeyroux and Pierre Leleu }, title = {Recursion over Objects of Functional Type}, journal = {Mathematical Structures in Computer Science}, year = {2001}, volume = 11, pages = "555-572", publisher = cambridge-press } @InProceedings{despeyroux+:functional-preprint, author = {{Jo\"{e}lle} Despeyroux and Pierre Leleu }, title = {Recursion over Objects of Functional Type}, booktitle = {Proceedings of the Types Working Group Meeting at Kloster Irsee, 1998}, year = 1999, number = 1657, series = lncs, address = {Berlin}, publisher = springer } @InProceedings{despeyroux+:modal, author = {{Jo\"{e}lle} Despeyroux and Pierre Leleu }, title = {A modal lambda-calculus with iteration and case constructs}, booktitle = {Proceedings of the Types Working Group Meeting at Kloster Irsee, 1998}, year = 1999, number = 1657, series = lncs, address = berlin, publisher = springer } @inproceedings{despeyroux+:ho-recursion, author = "{Jo\"{e}lle} Despeyroux and Frank Pfenning and {Carsten Sch\"{u}rmann}", title = "Primitive Recursion for Higher-Order Abstract Syntax", booktitle = o3 # " " # tlca, year = 1997, month = apr, address = "Nancy, France", pages = "147--163", series = lncs, volume = 1210, publisher = springer, annote = "Extended version published as CMU technical report CMU-CS-96-172.", } @inproceedings{dimock+:flow-transforms, title = "Strongly Typed Flow-Directed Representation Transformations", author = "Allyn Dimock and Robert Muller and Franklyn Turbak and J.~B.~Wells", booktitle = 1997 # " " # icfp, year = 1997, month = jun, address = "Amsterdam", pages = "11--24", } @InCollection{dobson91, author = {John E. Dobson}, title = {Information and Denial of Service}, booktitle = {Database Security V: Status and Prospects}, series = {IFIP Transactions}, volume = {A-6}, pages = {21--46}, year = 1991 } @inproceedings{dubois+:extensional-poly, author = "Catherine Dubois and Fran\c{c}ois Rouaix and Pierre Weis", title = "Extensional Polymorphism", booktitle = o22 # " " # popl, address = "San Francisco", month = jan, year = 1995, pages = "118--129", } @inproceedings{duggan:marshalling, author = "Dominic Duggan", title = "A Type-Based Semantics for User-Defined Marshalling in Polymorphic Languages", booktitle = o2 # " " # tic, year = 1998, month = mar, } @InProceedings{duggan:tmal, author = {Dominic Duggan}, title = {Sharing in Typed Module Assembly Language}, booktitle = {Types in Compilation : Third International Workshop, {TIC} 2000 Montreal; Canada, September 21, 2000; Revised Selected Papers}, year = 2001, editor = {R. Harper}, pages = {85--116}, volume = 2071, series = lncs, address = {Berlin}, publisher = {Springer} } @book{dummett:intuitionism, author = "Michael Dummett", title = "Elements of Intuitionism", publisher = "Clarendon Press", year = 1977, series = "Oxford Logic Guides", } @InCollection{dybjer:inductive, author = {Peter Dybjer}, title = {Inductive sets and families in {M}artin-{L}\"of's type theory and their set-theoretic semantics}, booktitle = {Logical Frameworks}, pages = {280--306}, year = 1991, editor = {Gerard Huet and Gordon Plotkin}, publisher = {Prentice Hall} } %% E %% @incollection{eifrig+:constrained-types, author = "J. Eifrig and S. Smith and V. Trifonov", title = "Type Inference for Recursively Constrained Types and its Application to {OOP}", booktitle = mfps, publisher = elsevier, series = "Electronic Notes in Theoretical Computer Science", volume = 1, year = 1995, } @BOOKLET{ELF, AUTHOR = {{T}ool {I}nterface {S}tandards {C}ommittee}, TITLE = {{E}xecutable and {L}inking {F}ormat ({ELF}) Specification}, MONTH = {May}, YEAR = {1995}, HOWPUBLISHED = {\url{http://x86.ddj.com/ftp/manuals/tools/elf.pdf}} } @InProceedings{engblom98optimize, author = {Jakob Engblom and Andreas Ermedahl and Peter Altenbernd}, title = {Facilitating worst-case execution time analysis of optimized code}, booktitle = {Proceedings of the 10th EuroMicro Workshop on Real-Time Systems}, year = 1998, address = {Berlin, Germany}, month = jun } @INPROCEEDINGS{EnglerKO95, TITLE = {{E}xokernel: an operating system architecture for application-level resource management}, AUTHOR = {Dawson R. Engler and M. Frans Kaashoek and James {O'Toole Jr.}}, BOOKTITLE = {Proceedings of the 15th {ACM} {S}ymposium on {O}perating {S}ystems {P}rinciples}, YEAR = {1995}, MONTH = {December}, ADDRESS = {Copper Mountain Resort, Colorado}, PAGES = {251--266}, URL = {http://www.pdos.lcs.mit.edu/papers/exokernel-sosp95.ps} } @InProceedings{erlingsson99sasi, author = {\'{U}lfar Erlingsson and Fred B. Schneider}, title = {{SASI} Enforcement of Security Policies: A Retrospective}, booktitle = {Proceedings of the 1999 New Security Paradigms Workshop}, year = 1999, address = {Caledon Hills, Ontario, Canada}, month = sep } %% F %% @Article{feferman62, author = {Solomon Feferman}, title = { Transfinite Recursive Progressions of Axiomatic Theories.}, journal = { Journal of Symbolic Logic}, year = 1962, volume = 27, number = 3, pages = {259--316}, month = sep } @inproceedings{ fegaras+:outer-space, author = "Leonidas Fegaras and Tim Sheard", title = "Revisiting Catamorphisms over Datatypes with Embedded Functions (or, Programs from Outer Space)", booktitle = o23 # popl, address = {St.~Petersburg Beach, {FL},{USA}}, pages = "284--294", year = 1996, annote = {Also: OGI Technical Report 95/014}, url = "citeseer.nj.nec.com/article/fegaras96revisiting.html" } % publisher = "ACM Press", % address = "New York", % booktitle = "Conf.\ Record 23rd {ACM} {SIGPLAN}/{SIGACT} Symp.\ % on Principles of Programming Languages, {POPL}'96, % St.~Petersburg Beach, {FL}, {USA}, 21--24 Jan.\ 1996", @InCollection{ferdinand98cache, author = {Christian Ferdinand and Reinhard Wilhelm}, title = {On predicting Data Cache Behavior for Real-Time systems}, booktitle = lctes, pages = "16--30", publisher = springer, year = 1998, editor = {Frank Muller and Azer Bestarvros}, volume = 1474, series = lncs, month = jun } @phdthesis{filinski:phd, author = "Andrzej Filinski", title = "Controlling Effects", year = 1996, month = may, school = cmu-cs, address = pgh-pa, } @inproceedings{fischer:cps, author = "M.J. Fischer", title = "Lambda calculus schemata", booktitle = "ACM Conference on Proving Assertions About Programs, SIGPLAN Notices 7(1)", year = 1972, pages = "104--109", } @inproceedings{flatt+:units, author = "Matthew Flatt and Matthias Felleisen", title = "Units: Cool Modules for {HOT} Languages", booktitle = 1998 # " " # pldi, pages = "236--248", year = 1998, month = jun, address = "Montreal, Canada", } @InProceedings{freeman91refinement, author = {Tim Freeman and Frank Pfenning}, title = {Refinement Types for {ML}}, booktitle = 1991 # " " # pldi, pages = {268--277}, year = 1991, address = {Toronto, Canada}, month = jun } @InBook{friedman:equality, author = {H. Friedman}, editor = {R. Parikh}, chapter = {Equality between functionals}, title = {Logic Colloquium}, publisher = {Springer-Verlag}, year = 1975, address = {Berlin}, pages = {22--37} } %% G %% @Article{PittsAM:newaas-jv, author = {M. J. Gabbay and A. M. Pitts}, title = {A New Approach to Abstract Syntax with Variable Binding}, journal = {Formal Aspects of Computing}, year = 2001, volume = 13, pages = {341--363} } @incollection{gallier:candidates-of-reducibility, author = "Jean H. Gallier", title = "On {Girard's} ``{Candidats} de {Reductibilit{\'{e}}}''", booktitle = "Logic and Computer Science", pages = "123--203", year = 1990, series = "The {APIC} Series", volume = 31, editor = "P. Odifreddi", publisher = academic, } @InProceedings{gapayev+:regular-object-types, author = {Vladimir Gapeyev and Benjamin Pierce}, title = {Regular Object Types}, booktitle = {Proc. 10th International Workshops on Foundations of Object-Oriented Languages, FOOL '03}, year = 2003, address = {New Orleans, LA, USA}, month = jan } @InCollection{gandy:turing-proof, author = {Robin O. Gandy}, editor = "J. Roger Seldin and Jonathan R. Hindley", title = { An Early Proof of Normalization by {A.M. Turing}}, booktitle = { Introduction to Combinators and $\lambda$-Calculus }, publisher = cambridge-press, year = 1986, series = {London Mathematical Society Student Texts}, address = {Cambridge}, pages = {453--455 } } @InProceedings{garrigue:poly-variants, author = {J. Garrigue}, title = {Programming with polymorphic variants}, booktitle = {ML Workshop}, url = "citeseer.nj.nec.com/garrigue98programming.html", year = 1998, month = sep } @inproceedings{gifford+:effects, title = "Integrating functional and imperative programming", author = "D. K. Gifford and J. M. Lucassen", booktitle = "{ACM} Conference on {Lisp} and Functional Programming", address = "Cambridge, Massachusetts", month = aug, year = 1986 } @article{ghelli:fsub-divergence, author = "Giorgio Ghelli", title = "Divergence of {$F_{\leq}$} type checking", journal = "Theoretical Computer Science", volume = 139, number = "1,2", pages = "131--162", year = 1995, } @phdthesis{ghelli:phd, author = "Giorgio Ghelli", title = "Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism", school = "Dipartimento di Informatica, Universit\`{a} di Pisa", year = 1990, month = mar, } @book{girard+:proofs-and-types, author = "Jean-Yves Girard and Yves Lafont and Paul Taylor", title = "Proofs and Types", publisher = cambridge-press, year = 1988, } @inproceedings{girard:cut-elimination, author = "Jean-Yves Girard", title = "Une extension de l'interpr\'{e}tation de {G\"{o}del} \`{a} l'analyse, et son application \`{a} l'\'{e}limination de coupures dans l'analyse et la th\'{e}orie des types", editor = "J. E. Fenstad", booktitle = "Proceedings of the Second Scandinavian Logic Symposium", pages = "63--92", year = 1971, publisher = "North-Holland Publishing Co.", } @article{girard:linear, title = "Linear Logic", author = "Jean-Yves Girard", journal = "Theoretical Computer Science", year = 1987, volume = 50, pages = "1--102", } @phdthesis{girard:phd, author = "Jean-Yves Girard", title = "Interpr\'{e}tation fonctionelle et \'{e}limination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur", school = "Universit\'{e} Paris VII", year = 1972, } @InProceedings{glew:branded, author = {Neal Glew}, title = {Type Dispatch for Named Hierarchical Types}, booktitle = 1999 # " " # icfp, pages = {172--182}, year = 1999, address = {Paris, France}, month = sep } @inproceedings{glew+:linking, author = "Neal Glew and Greg Morrisett", title = "Type-Safe Linking and Modular Assembly Language", year = 1999, booktitle = o26 # " " # popl, month = jan, address = {San Antonio, TX}, pages = {250--261} } @Article{gligor84:os, author = {Virgil D. Gligor}, title = {A Note on Denial-of-Service in Operating Systems}, journal = {IEEE Transactions on Software Engineering}, year = 1984, volume = 10, number = 3, pages = {320--324} } @inproceedings{gligor86:_denial_servic_comput_networ, author = {Virgil D. Gligor}, title = {On Denial-of-Service in Computer Networks}, booktitle = {Proceedings of the Second International Conference on Data Engineering, February 5-7, 1986, Los Angeles, California, USA}, publisher = {IEEE Computer Society}, year = 1986, isbn = {0-8186-0655-X}, pages = {608-617}, crossref = {DBLP:conf/icde/86}, bibsource = {DBLP, http://dblp.uni-trier.de} } @Article{godel:incompleteness, author = {Kurt Godel}, title = {\"{U}ber formal unentschiedbare S\"atze der Principia Mathematica und verwandter Systeme, {I}}, journal = {Monatshefte f\"ur Mathematik und Physik}, year = 1931, volume = 38, pages = {173--98} } @InProceedings{godfrey98:_secur_portab_datab_exten, author = {M. Godfrey and T. Mayr and P. Seshadri and T. von Eiken}, title = {Secure and Portable Database Extensibility}, booktitle = sigmod, year = 1998, volume = 27, number = 2, series = {SIGMOD Record}, month = jun } @book{gordon+:hol, author = "Michael J. C. Gordon and Tom F. Melham", title = "Introduction to {HOL}: A Theorem Proving Environment for Higher-Order Logic", publisher = cambridge-press, year = 1993, } @inproceedings{gordon+:imperative-objs, author = "Andrew D. Gordon and Paul D. Hankin and {S\o ren} B. Lassen", title = "Compilation and Equivalence of Imperative Objects", booktitle = "Foundations of Software Technology and Theoretical Computer Science", year = 1997, month = dec, series = lncs, volume = 1346, publisher = springer, } @book{gordon+:lcf, author = "Michael J. Gordon and Arthur J. Milner and Christopher P. Wadsworth", title = "Edinburgh {LCF}: A Mechanised Logic of Computation", publisher = springer, series = lncs, year = 1979, volume = 78, } @book{gosling+:java, author = "James Gosling and Bill Joy and Guy Steele", title = "The {Java} Language Specification", publisher = addison, year = 1996, } @inproceedings{gougen+:datatypes, author = "J. A. Goguen and J. W. Thatcher and E. G. Wagner", title = "An initial algebra approach to the specification, correctness and implementation of abstract data types.", editor = "R. T. Yeh", booktitle = "Current Trends in Programming Methodology IV: Data Structuring", pages = "80--144", publisher = "Prentice Hall", year = 1978 } @InProceedings{green:java-reflection, author = {Dale Green}, editor = {Mary Campione and Kathy Walrath and Alison Huml and Tutorial Team}, booktitle = {The Java Tutorial Continued: The Rest of the JDK(TM) }, title = {Trail: The Reflection {API}}, publisher = {Addison-Wesley Pub Co}, year = 1998, note = {\url{http://java.sun.com/docs/books/tutorial/reflect/index.html}} } @Article{grossman:sta, author = {Dan Grossman and Greg Morrisett and Steve Zdancewic}, title = {Syntactic Type Abstraction}, journal = toplas, year = 2000, volume = 22, number = 6, pages = {1037--1080}, month = nov } @InProceedings{grossman+:tic, author = {Dan Grossman and Greg Morrisett}, title = {Scalable Certification of Native Code: Experience from Compiling to TALx86}, booktitle = "Preliminary Proceedings of the Third " # tic, year = 2000, address = {Montreal, CA}, month = sep, note = {Extended version published as Cornell University Computer Science technical report TR2000-1783} } @TechReport{grossman00, author = {Dan Grossman and Greg Morrisett}, title = {Scalable Certification of Native Code: Experience from Compiling to TALx86}, institution = cornell-cs, year = 2000, number = {TR2000-1783}, month = feb } @book{gunter+:theoretical-oop, editor = "Carl A. Gunter and John C. Mitchell", title = "Theoretical Aspects of Object-Oriented Programming", publisher = mit-press, year = 1994, address = cam-ma } %% H %% @article{ hall96type, author = "Cordelia V. Hall and Kevin Hammond and Simon L. {Peyton Jones} and Philip L. Wadler", title = "Type Classes in {H}askell", journal = "ACM Transactions on Programming Languages and Systems", volume = "18", number = "2", month = mar, publisher = "ACM Press", pages = "109--138", year = "1996" } # url = "citeseer.nj.nec.com/article/hall96type.html" @TechReport{harrison:survey, author = {John Harrison}, title = {Metatheory and Reflection in Theorem Proving: A Survey and Critique}, institution = {SRI}, number = {CRC-053}, month = feb, year = 1995 } @inproceedings{harper+:cps, author = "Robert Harper and Mark Lillibridge", title = "Explicit Polymorphism and {CPS} Conversion", booktitle = o20 # " " # popl, month = jan, year = 1993, pages = "206--219", } @inproceedings{harper+:ita, author = "Robert Harper and Greg Morrisett", title = "Compiling Polymorphism Using Intensional Type Analysis", pages = "130--141", booktitle = o22 # " " # popl, address = "San Francisco", month = jan, year = 1995, } @article{harper+:lf, author = "Robert Harper and Furio Honsell and Gordon Plotkin", title = "A Framework for Defining Logics", journal = jacm, volume = 40, number = 1, month = jan, year = 93, pages = "143--184", } @inproceedings{harper+:phase, author = "Robert Harper and John C. Mitchell and Eugenio Moggi", title = "Higher-Order Modules and the Phase Distinction", booktitle = o17 # " " # popl, address = "San Francisco", month = jan, year = 1990, pages = "341--354" } @inproceedings{harper+:translucent, author = "Robert Harper and Mark Lillibridge", title = "A Type-Theoretic Approach to Higher-Order Modules with Sharing", booktitle = o21 # " " # popl, month = jan, year = 1994, address = "Portland, Oregon", pages = "123--137", } @incollection{harper+:tt-interp-sml, author = "Robert Harper and Chris Stone", title = "A Type-Theoretic Interpretation of {Standard} {ML}", booktitle = "Proof, Language and Interaction: Essays in Honour of Robin Milner", year = 1998, publisher = mit-press, note = "Extended version published as CMU technical report CMU-CS-97-147.", } @techreport{harper+:tt-interp-sml-tr, author = "Robert Harper and Chris Stone", title = "An Interpretation of {Standard} {ML} in Type Theory", institution = cmu-cs, year = 1997, month = jun, number = "CMU-CS-97-147", } @article{harper+:type-structure-sml, author = "Robert Harper and John C. Mitchell", title = "On the Type Structure of {Standard ML}", journal = toplas, year = 1993, volume = 15, number = 2, pages = "211--252", month = apr, } @article{harper+:typecheck-univ, author = "Robert Harper and Robert Pollack", title = "Type Checking with Universes", journal = tcs, volume = 89, year = 1991, pages = "107--136", } @inproceedings{harper+:typical-ambiguity, author = "Robert Harper and Robert Pollack", title = "Type Checking, Universe Polymorphism, and Typical Ambiguity in the Calculus of Constructions", booktitle = "Proceedings of the International Joint Conference on Theory and Practice of Software Development", address = "Barcelona", year = 1989, month = mar, series = lncs, volume = 352, publisher = springer, } @article{harper:types-over-op-semant, author = "Robert Harper", title = "Constructing Type Systems over an Operational Semantics", journal = "Journal of Symbolic Computation", year = 1992, volume = 14, pages = "71--84", } @inproceedings{harper:tdtt, author = "Daniel R. Licata and Robert Harper", title = "2-Dimensional {Directed} {Type} {Theory}", year = 2011, booktitle = "MFPS XXVII: Mathematical Foundations of Programming Semantics" } @Unpublished{harper:notes, author = {Robert Harper}, title = {Programming Languages: Theory and Practice}, note = {Unpublished, draft available at \url{http://www.cs.cmu.edu/~rwh/plbook/}}, year = 2001 } @Article{hosoya+:xduce, author = {Haruo Hosoya and Benjamin C. Pierce}, title = {Regular expression pattern matching for {XML}}, journal = jfp, year = 2002, volume = 13, number = 4 } @TechReport{peterson+:tilt, author = {Leaf Petersen and Perry Cheng and Robert Harper and Chris Stone}, title = {Implementing the {TILT} Internal Language}, institution = { Carnegie Mellon University Computer Science}, year = 2000, number = {CMU-CS-00-180}, month = dec } @unpublished{hickey:tt-obj-semant, author = "Jason J. Hickey", title = "A Semantics of Objects in Type Theory", note = "Unpublished manuscript", year = 1997, } @inproceedings{hickey:very-dependent-type, author = "Jason J. Hickey", title = "Formal Objects in Type Theory Using Very Dependent Types", booktitle = "Foundations of Object Oriented Languages 3", year = 1996, } @Article{hinze:polytypic-journal, author = {Ralf Hinze}, title = {Polytypic values possess polykinded types}, journal = {Science of Computer Programming}, year = 2002, volume = 43, number = {2--3}, pages = {129--159}, note = {MPC Special Issue} } @InProceedings{hinze:polytypic, author = {Ralf Hinze}, title = {Polytypic values possess polykinded types}, booktitle = {Proceedings of the Fifth International Conference on Mathematics of Program Construction (MPC 2000)}, year = 2000, editor = {Roland Backhouse and J.N. Oliveira}, address = {Ponte de Lima, Portugal}, month = jul, pages = "2--27" } @Incollection{hinze+:derivable, author = {Ralf Hinze and Simon {Peyton Jones}}, title = {Derivable Type Classes}, booktitle = { Proceedings of the Fourth {H}askell Workshop, Montreal, Canada, September 17, 2000}, year = 2000, editor = {Graham Hutton}, series = { Electronic Notes in Theoretical Computer Science}, publisher = { Elsevier Science}, volume = {41.1}, month = aug, annotation = {no page number.} } @InProceedings{hinze+:type-indexed-datatypes, author = {Ralf Hinze and Johan Jeuring and Andres L\"oh}, title = {Type-indexed data types}, booktitle = {Proceedings of the Sixth International Conference on Mathematics of Program Construction (MPC 2002)}, year = 2002, editor = {Eerke Boiten, Bernhard M\"oller}, address = { Dagstuhl, Germany }, month = jul, pages = {148--174} } @article{luo:coercions, author = {Zhaohui Luo}, title = {Coercions in a polymorphic type system}, journal = {Mathematical Structures in Computer Science}, volume = {18}, number = {4}, year = {2008}, pages = {729-751}, ee = {http://dx.doi.org/10.1017/S0960129508006804}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{chakravarty+:accelerate, author = {Chakravarty, Manuel M.T. and Keller, Gabriele and Lee, Sean and McDonell, Trevor L. and Grover, Vinod}, title = {Accelerating {Haskell} array codes with multicore {GPU}s}, booktitle = {Proceedings of the sixth workshop on {Declarative} {Aspects} of {Multicore} {Programming}}, series = {DAMP '11}, year = {2011}, isbn = {978-1-4503-0486-3}, location = {Austin, Texas, USA}, pages = {3--14}, numpages = {12}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {arrays, data parallelism, dynamic compilation, gpgpu, haskell, skeletons}, } @article{henglein:coercions, author = {Henglein, Fritz}, title = {Dynamic typing: syntax and proof theory}, journal = {Sci. Comput. Program.}, volume = {22}, issue = {3}, month = {June}, year = {1994}, issn = {0167-6423}, pages = {197--230}, numpages = {34}, publisher = {Elsevier North-Holland, Inc.}, address = {Amsterdam, The Netherlands, The Netherlands}, } @INPROCEEDINGS{HicksMN01a, AUTHOR = {Michael Hicks and Jonathan T. Moore and Scott Nettles}, BOOKTITLE = {Proceedings of the {ACM SIGPLAN} Conference on Programming Language Design and Implementation}, TITLE = {Dynamic Software Updating}, MONTH = {June}, YEAR = 2001, PAGES = {13--23}, PUBLISHER = {{ACM}}, ABSTRACT = { Many important applications must run continuously and without interruption, yet must be changed to fix bugs or upgrade functionality. No prior general-purpose methodology for dynamic updating achieves a practical balance between flexibility, robustness, low overhead, and ease of use. We present a new approach for C-like languages that provides type-safe dynamic updating of native code in an extremely flexible manner (code, data, and types may be updated, at programmer-determined times) and permits the use of automated tools to aid the programmer in the updating process. Our system is based on \emph{dynamic patches} that both contain the updated code and the code needed to transition from the old version to the new. A novel aspect of our patches is that they consist of \emph{verifiable native code} (\emph{e.g.} Proof-Carrying Code~\cite{necula:pcc} or Typed Assembly Language~\cite{morrisett+:tal}), which is native code accompanied by annotations that allow on-line verification of the code's safety. We discuss how patches are generated mostly automatically, how they are applied using dynamic-linking technology, and how code is compiled to make it updateable. To concretely illustrate our system, we have implemented a dynamically-updateable web server, FlashEd. We discuss our experience building and maintaining FlashEd. Performance experiments show that for FlashEd, the overhead due to updating is typically less than 1 percent. }, URL = {http://www.cis.upenn.edu/~mwh/papers/dyn_update.ps} } @PHDTHESIS{Hicks01, AUTHOR = {Michael Hicks}, TITLE = {Dynamic Software Updating}, YEAR = 2001, MONTH = {August}, SCHOOL = {Department of Computer and Information Science, University of Pennsylvania}, URL = {http://www.cis.upenn.edu/~mwh/papers/thesis.pdf} } @InProceedings{hicks98:_plan, author = {M. Hicks and P. Kakkar and J. Moore and C. Gunter and S. Nettles}, title = {{PLAN:} A Programming Language for Active Networks}, booktitle = o3 # " " # icfp, pages = "86--93", year = 1998 } @article{hoffman+:unifying-objects, author = "Martin Hofmann and Benjamin Pierce", title = "A Unifying Type-Theoretic Framework for Objects", journal = jfp, year = 1995, month = oct, volume = 5, number = 4, pages = "593--635" } @InProceedings{hofmann00esop, author = {Martin Hofmann}, title = {A Type System for Bounded Space and Functional in-place update}, booktitle = esop, year = 2000 } @InProceedings{hofmann99lics, author = {Martin Hofmann}, title = {Linear Types and non-size increasing polynomial computation}, booktitle = lics, year = 1999, address = {Trento, Italy}, month = jul } @MISC{HotJava, KEY = {hotjava}, TITLE = {HotJava Browser}, NOTE = {\url{http://java.sun.com/products/hotjava/index.html}} } @techreport{hook+:impred-strong-sum, author = "James G. Hook and Douglas J. Howe", title = "Impredicative Strong Existential Equivalent to Type:Type", institution = cornell-cs, year = 1986, month = jun, number = "TR 86-760", } @incollection{hook:understanding-russell, author = "James G. Hook", title = "Understanding {Russell}---A First Attempt", booktitle = "Semantics of Data Types", series = lncs, volume = 173, publisher = springer, year = 1984, } @InProceedings{hornof99rtcg, author = {Luc Hornof and Trevor Jim}, title = {Certifying compilation and run-time code generation}, booktitle = pepm, year = 1999, month = jan } @incollection{howard:formulas-as-types, author = "W. Howard", title = "The Formulas-as-Types Notion of Construction", booktitle = "To {H.B.} {Curry}: Essays on Combinatory Logic, Lambda-Calculus and Formalism", editor = "J. P. Seldin and J. R. Hindley", pages = "479--490", publisher = "Academic Press", year = 1980, } @InBook{howard73logical, author = {W. Howard}, chapter = {Hereditarily majorizable functionals}, title = {Mathematical Investigation of Intuistionistic Arithmetic and Analysis}, year = 1973, number = {LNM}, pages = {454--461}, address = {Berlin}, publisher = {Springer} } @techreport{howe:embedding-hol-in-nuprl, author = "Douglas J. Howe", title = "Semantic Foundations for Embedding {HOL} in {Nuprl}", institution = "Bell Labs", year = 1996, } @inproceedings{howe:girard-paradox, author = "Douglas J. Howe", title = "The Computational Behaviour of {G}irard's Paradox", booktitle = o2 # " " # lics, year = 1987, month = jun, pages = "205--214", address = ith-ny, } @inproceedings{howe:squiggle-eq, author = "Douglas J. Howe", title = "Equality in Lazy Computation Systems", booktitle = o4 # " " # lics, year = 1989, } @article{hudak+:haskell, author = "Paul Hudak and Simon {Peyton Jones} and Philip Wadler", title = "Report on the Programming Language {Haskell}, version 1.2", journal = "SIGPLAN Notices", volume = 27, number = 5, year = 1992, month = may, } @InProceedings{hughes96:_provin_correc_react_system_using_sized_types, author = {John Hughes and Lars Pareto and Amr Sabry}, title = {Proving the Correctness of Reactive Systems Using Sized Types}, booktitle = o23 # " " # popl, year = 1996, pages = "410--423", month = jan } @Manual{hugs, title = {Hugs 98 : A functional programming system based on {H}askell 98 : User Manual}, author = {Mark P Jones and Alastair Reid}, organization = {Yale Haskell Group and Oregon Graduate Institute of Science and Technology}, note = {Available at \url{http://cvs.haskell.org/Hugs/downloads/hugs.pdf}}, month = sep, year = 1999 } @InProceedings{hurkens:paradox, author = {Antonious J. C. Hurkens }, title = {A simplification of {Girard's} Paradox}, year = 1995, booktitle = "Second International Conference on Typed Lambda Calculi and Applications, TLCA '95", editor = {Mariangiola Dezani-Ciancaglini and Gordon Plotkin}, volume = 902, series = lncs, address = {Edinburgh, United Kingdom}, month = apr, publisher = springer, pages = {266--278} } %% I %% @techreport{igarashi:admissibility, author = "Shigeru Igarashi", title = "Admissibility of Fixed-Point Induction in First-Order Logic of Typed Theories", institution = "Computer Science Department, Stanford University", year = 1972, month = may, number = "AIM-168", } %% J %% @manual{jackson:nuprl-manual, title = "The {N}uprl Proof Development System, Version 4.1", author = "Paul Jackson", organization = cornell-cs, webnote = "Available at http://www.cs.cornell.edu/Info/Projects/NuPrl/html/nuprldocs.html", year = 1994, } @phdthesis{jackson:phd, author = "Paul Bernard Jackson", title = "Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra", school = cornell-cs, month = jan, year = 1995, address = ith-ny, } @PhdThesis{jansson:phd, author = {Patrik Jansson}, title = {Functional Polytypic Programming}, school = {Chalmers University of Technology and Goteborg University}, year = 2000 } @InProceedings{jansson97polyp, author = {Patrick Jansson and Johan Jeuring}, title = {{PolyP}---{A} Polytypic Programming Language Extension}, booktitle = o24 # " " # popl, pages = {470--482}, year = 1997, address = {Paris, France} } @InProceedings{janssonjeuringWGP00:rewriting, author = {Jansson, Patrik and Jeuring, Johan}, title = {A Framework for Polytypic Programming on Terms, with an Application to Rewriting}, booktitle = "Workshop on Generic Programming (WGP2000), Ponte de Lima, Portugal", publisher = "Utrecht University", note = "Technical Report UU-CS-2000-19", year = 2000 } @InProceedings{jansson+:polytypic-compression, author = {Patrik Jansson and Johan Jeuring}, title = {Polytypic Compact Printing and Parsing}, booktitle = esop, pages = {273-287}, year = 1999, volume = 1576, series = lncs } @Article{jansson+:polytypic-unification, author = {Patrik Jansson and Johan Jeuring}, title = {Functional Pearl: Polytypic Unification}, journal = jfp, year = 1998, volume = 8, number = 5, month = sep, pages = {527--536} } @article{jategaonkar+:ext-pattern-subtypes, author = "Lalita A. Jategaonkar and John C. Mitchell", title = "Type Inference with Extended Pattern Matching and Subtypes", journal = "Fundamenta Informaticae", year = 1993, volume = 19, pages = "127--166", note = "{\it Preliminary version appeared in 1988 {ACM} Conference on Lisp and Functional Programming}", } @Misc{JavaBeans, key = {JavaBeans}, title = {{JavaBeans}: The Only Component for {Java} Technology}, month = may, year = 2002, note = {\url{http://java.sun.com/products/javabeans/}} } @MISC{JavaClassloading96, KEY = {javaclass}, TITLE = {Basics of Java class loaders}, YEAR = {1996}, NOTE = {\url{http://www.javaworld.com/javaworld/jw-10-1996/jw-10-indepth.html}} } @Article{jay+:fml, author = {C. Barry Jay and Gianna Bell\`{e} and Eugenio Moggi}, title = {Functorial {ML} }, journal = jfp, year = 1998, volume = 8, number = 6, pages = {573--619}, month = nov } @article{ jay95semantics, author = "C. Barry Jay", title = "A Semantics for Shape", journal = "Science of Computer Programming", volume = "25", number = "2--3", pages = "251--283", year = "1995", url = "citeseer.nj.nec.com/71598.html" } @Article{jay:fish, author = {C.B. Jay}, title = {Programming in {FISh} }, journal = {International Journal on Software Tools for Technology Transfer}, year = 1999, volume = 2, pages = {307--315} } @unpublished{ jim99type, author = "Trevor Jim and Jens Palsberg", title = "Type inference in systems of recursive types with subtyping", year = "1999", note = { Available at \url{citeseer.nj.nec.com/jim97type.html}} } @Article{johann:short-cut, author = {Patricia Johann}, title = {A Generalization of Short-Cut Fution and its Correctness Proof}, journal = hosc, year = 2002, volume = 15, pages = {273--300} } @techreport{jones:gofer-impl, author = "Mark P. Jones", title = "The Implementation of the {G}ofer Functional Programming System", institution = yale-cs, year = 1994, month = may, type = "Research Report", number = "YALEU/DCS/RR-1030", } @phdthesis{jones:phd, author = "Mark P. Jones", title = "Qualified Types: Theory and Practice", school = "Oxford University Computing Laboratory", year = 1992, month = jul, } @techreport{jones:qualified-type-coherence, author = "Mark P. Jones", title = "Coherence for Qualified Types", institution = yale-cs, year = 1993, month = sep, type = "Research Report", number = "YALEU/DCS/RR-989", } @incollection{ jones:qualified-types, author = "Mark P. Jones", title = "A Theory of Qualified Types", booktitle = "{ESOP} '92, 4th European Symposium on Programming, Rennes, France, February 1992, Proceedings", volume = 582, publisher = "Springer-Verlag", address = "New York, N.Y.", editor = "Bernd Krieg-Bruckner", pages = "287--306", year = 1992, url = "citeseer.nj.nec.com/jones92theory.html" } @Article{jones:ho-poly, author = {Mark P. Jones}, title = {A system of constructor classes: overloading and implicit higher-order polymorphism }, journal = jfp, year = 1995, volume = 5, number = 1, month = jan } @InProceedings{jones:fundeps, author = {Mark P. Jones}, title = {Type Classes with Functional Dependencies}, booktitle = {Proceedings of the 9th European Symposium on Programming, ESOP 2000, Berlin, Germany}, year = 2000, number = 1782, series = {LNCS}, publisher = {Springer-Verlag} } @inproceedings{ jones97firstclass, author = "Mark P. Jones", title = "First-class Polymorphism with Type Inference", booktitle = "Conference Record of {POPL}~'97: The 24th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages", month = "15--17", address = "Paris, France", pages = "483--496", year = "1997", url = "citeseer.nj.nec.com/451312.html" } @inproceedings{jouvelot+:effects, author = "Pierre Jouvelot and D. K. Gifford", title = "Algebraic reconstruction of types and effects", booktitle = eighteenth # popl, year = 1991, month = jan, pages = "303--310" } @InProceedings{juering:polytypic-pattern, author = {J. Jeuring}, title = { Polytypic pattern matching}, booktitle = "FPCA95: " # fpca, pages = {238--248}, year = 1995 } %% K %% @inproceedings{kamin:smalltalk-semantics, author = "Samuel Kamin", title = "Inheritance in {S}malltalk-80: A Denotational Definition", booktitle = o15 # " " # popl, year = 1988, month = jan, pages = "80--87", address = "San Diego", } @Article{r5rs, author = {Richard Kelsey and William Clinger and Jonathan Rees, editors}, title = { {Revised$^5$} Report on the Algorithmic Language {S}cheme }, journal = {Higher-Order and Symbolic Computation}, year = 1998, volume = 11, number = 1, month = sep, pages = {7--105} } @inproceedings{kennedy:dimensions, author = "Andrew J. Kennedy", title = "Relational Parametricity and Units of Measure", booktitle = o24 # " " # popl, year = 1997, month = jan, address = "Paris", pages = "442--455", } @InProceedings{kennedy+:c-sharp-generics, author = {Andrew Kennedy and Don Syme}, title = {Design and Implementation of Generics for the {.NET} Common Language Runtime }, booktitle = proc # 2001 # pldi, pages = {1--12}, year = 2001, address = {Snowbird, Utah, USA}, month = jun } @Book{k&r, author = {Brian W. Kernighan and Dennis M. Ritchie}, title = {The C Programming Language, Second Edition}, publisher = {Prentice Hall, Inc.}, year = 1988 } @inproceedings{kieburtz:taming-effects, author = "Richard B. Kieburtz", title = "Taming Effects with Monadic Typing", booktitle = 1998 # " " # icfp, year = 1998, month = sep, address = "Baltimore", pages = "51--62", } @Incollection{kiczales:aop, author = {Gregor Kiczales and John Lamping and Anurag Mendhekar and Chris Maeda and Cristina Videira Lopes and Jean-Marc Loingtier and John Irwin}, title = {Aspect-Oriented Programming}, booktitle = { Proceedings of the European Conference on Object-Oriented Programming (ECOOP)}, year = 1997, volume = 1241, series = lncs, month = jun, editor = "Mehmet Ak\c{s}it and Satoshi Matsuoka", pages = "220--242", publisher = {Springer-Verlag} } @InProceedings{kim99impacts, author = {Sung-Kwan Kim and Rhan Ha and Sang Lyul Min}, title = {Analysis of the Impacts of Overestimation Sources on the Accuracy of Worst Case Timing Analysis}, booktitle = {IEEE Real-Time Systems Symposium}, pages = {22--31}, year = 1999, address = {Phoeniz, AZ}, month = {December}, organization = {IEEE Computer Society} } @inproceedings{kranz+:orbit, author = "David Kranz and R. Kelsey and J. Rees and P. R. Hudak and J. Philbin and N. Adams", title = "{ORBIT}: An Optimizing Compiler for {S}cheme", booktitle = "Proceedings of the {ACM SIGPLAN} '86 Symposium on Compiler Construction", year = 1986, month = jun, pages = "219--233", } @techreport{kreitz:embedding, author = "Christoph Kreitz", title = "Formal Reasoning about Communications Systems {I}", institution = cornell-cs, year = 1997, } @inproceedings{ krishnamurthi+:extensible-visitor, author = "Shriram Krishnamurthi and Matthias Felleisen and Daniel P. Friedman", title = "Synthesizing Object-Oriented and Functional Design to Promote Re-use", booktitle = "European Conference on Object Oriented Programming", pages = "91--113", year = "1998", url = "citeseer.nj.nec.com/krishnamurthi98synthesizing.html" } @TechReport{Kozen98, author = {Dexter Kozen}, title = {Efficient Code Certification}, institution = {Department of Computer Science, Cornell University}, year = 1998, number = {98-1661}, address = {Ithaca, NY 12853-7501}, month = {January} } @inproceedings{ kozen93efficient, author = "Dexter Kozen and Jens Palsberg and Michael I. Schwartzbach", title = "Efficient Recursive Subtyping", booktitle = "Conference Record of the Twentieth Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages", address = "Charleston, South Carolina", pages = "419--428", year = "1993", url = "citeseer.nj.nec.com/article/kozen95efficient.html" } %% L %% @TechReport{lampson:cedar, author = {Butler Lampson}, title = {A description of the {C}edar language}, institution = {Xerox Palo Alto Research Center}, year = 1983, number = {CSL-83-15} } @article{landin:closure, author = "P. J. Landin", title = "The mechanical evaluation of expressions", journal = "Computer J.", volume = 6, number = 4, pages = "308--320", year = 1964, } @article{launchbury+:haskell-state, author = "John Launchbury and Simon {Peyton Jones}", title = "State in {Haskell}", journal = "Lisp and Symbolic Computation", volume = 8, number = 4, month = dec, year = 1995, pages = "293--341", } @inproceedings{launchbury+:param-unbox, author = "John Launchbury and Ross Paterson", title = "Parametricity and Unboxing with Unpointed Types", booktitle = o6 # " " # esop, year = 1996, month = apr, address = "{Link\"{o}ping}, Sweden", pages = "204--218", series = lncs, volume = 1058, publisher = springer, } @inproceedings{ lebotlan-remy:mlf-icfp, author = {Le Botlan, Didier and Remy, Didier}, title = "{MLF}: Raising {ML} to the Power of {S}ystem-{F}", booktitle = {Proceedings of the International Conference on Functional Programming ({ICFP} 2003), Uppsala, Sweden}, year = {2003}, publisher = {ACM Press}, pages = {27--38}, month = {aug}, pdf= {http://pauillac.inria.fr/~remy/work/mlf/icfp.pdf}, html= {http://pauillac.inria.fr/~remy/work/mlf/}, url = {citeseer.nj.nec.com/564799.html} } @inproceedings{leroy:applicative-functors, author = "Xavier Leroy", title = "Applicative Functors and Fully Transparent Higher-Order Modules", booktitle = o22 # " " # popl, year = 1995, month = jan, address = "San Francisco", } @inproceedings{leroy:manifest, author = "Xavier Leroy", title = "Manifest Types, Modules and Separate Compilation", booktitle = o21 # " " # popl, year = 1994, month = jan, address = "Portland, Oregon", pages = "109--122", } @manual{leroy:ocaml-manual, title = "The {O}bjective {C}aml System, Release 1.00", author = "Xavier Leroy", year = 1996, organization = inria, webnote = "Available at http://pauillac.inria.fr/ocaml", } @inproceedings{leroy:unbox, author = "Xavier Leroy", title = "Unboxed objects and polymorphic typing", booktitle = o19 # " " # popl, year = 1992, pages = "177-188", } @inproceedings{leroy:unbox-effectiveness, author = "Xavier Leroy", title = "The Effectiveness of Type-Based Unboxing", booktitle = tic, year = 1997, month = jun, address = "Amsterdam", organization = "{ACM SIGPLAN}", note = "Published as {B}oston {C}ollege Computer Science Department Technical Report BCCS-97-03", } @Article{leroy+:exceptions, author = {Xavier Leroy and F. Pessaux}, title = {Type-based analysis of uncaught exceptions}, journal = toplas, year = 2000, volume = 22, number = 2, pages = {340--377} } @incollection{ leroy91dynamics, author = "Xavier Leroy and Michel Mauny", title = "Dynamics in {ML}", booktitle = "Functional Programming Languages and Computer Architecture, 5th {ACM} Conference", volume = "523", publisher = "Springer-Verlag", address = "Berlin, Heidelberg, New York", editor = "J. Hughes", pages = "406--426", year = "1991", url = "citeseer.nj.nec.com/313297.html" } @InProceedings{leroy+:dynamics, author = {Xavier Leroy and Michel Mauny}, title = {Dynamics in {ML}}, booktitle = {Functional Programming Languages and Computer Architecture}, pages = {406-426}, year = 1991, editor = {J. Hughes}, number = 523, series = {Lecture Notes in Computer Science}, month = aug, publisher = {Springer-Verlag} } @string{popl00="Proceedings of the 27th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, Boston, Massachusetts"} @inproceedings{lewis+:implicit-params ,author="Jeffrey Lewis and Mark Shields and Erik Meijer and John Launchbury" ,title="Implicit Parameters: Dynamic Scoping with Static Types" ,booktitle=popl00 ,year="2000" ,month="Jan" ,pages="108--118" } @InProceedings{liedke+97:webos, author = {Jochen Liedtke and Nyeem Islam and Trent Jaeger}, title = {Preventing Denial-of-Service Attacks on a $\mu$-Kernel for web {OS}es}, booktitle = o6 # " " # hotos, year = 1997 } @article{liedtke95:cheap_time, author = {Jochen Liedtke}, title = {A Short Note on Cheap Fine-grained Time Measurement}, journal = {ACM Operating Systems Review}, pages = {31--34}, year = 95, volume = 29, number = 3, month = {July} } @phdthesis{lillibridge:phd, author = "Mark Lillibridge", title = "Translucent Sums: A Foundation for Higher-Order Module Systems", year = 1997, month = may, address = pgh-pa, school = cmu-cs, } @InProceedings{lim94risc, author = {Sung-Soo Lim and Young Hyun Bae and Gyu Tae Jang and Byung-Do Rhee and Sang Lyul Min and Chang Yun Park and Heonshik Shin and Kunsoo Park and Chong Sang Kim}, title = {An Accurate Worts Case Timing Analysis Technique for {RISC} Processors}, booktitle = o15 # " " # rtss, pages = {97--108}, year = 1994 } @book{lindholm+:jvm, title = "The {Java} Virtual Machine Specification", author = "Tim Lindholm and Frank Yellin", publisher = addison, year = 1996, } @MISC{LinuxDynlink95, KEY = {DLOPEN}, TITLE = {{DLOPEN}(3)}, howpublished = {{L}inux {P}rogrammer's {M}anual}, MONTH = {December}, YEAR = {1995} } @inproceedings{ liu98automatic, author = "Yanhong Liu and Gustavo Gomez", title = "Automatic accurate time-bound analysis for high-level languages", booktitle = lctes, publisher = springer, month = jun, series = lncs, volume = 1474, year = 1998 } @techreport{lucassen+:fx, author = "J. M. Lucassen and D. K. Gifford and P. Jouvelot and M. A. Sheldon", title = "{FX-87} Reference Manual", institution = "MIT Laboratory for Computer Science", number = "MIT/LCS/TR-407", month = sep, year = 1987, } @InCollection{lundqvist98integrating, author = {T. Lundqvist and P. Stenstrom}, title = {Integrating path and timing analysis using instruction-level simulation techniques}, booktitle = lctes, pages = {1--15}, publisher = springer, year = 1998, editor = {Frank Mueller and Azer Bestavros}, number = 1474, series = lncs } %% M %% @inproceedings{ma+:parametric-poly2, author = "QingMing Ma and John C. Reynolds", title = "Types, Abstraction, and Parametric Polymorphism, Part 2", booktitle = o7 # " " # mfps, year = 1991, month = mar, address = "Pittsburgh, Pennsylvania", series = lncs, volume = 598, publisher = springer, pages = "1--40", } @inproceedings{ma:parametricity, author = "QingMing Ma", title = "Parametricity as Subtyping", booktitle = o19 # " " # popl, year = 1992, month = jan, address = "Albuquerque, New Mexico", pages = "281--292", } @inproceedings{macqueen+:semantics-ho-functors, author = "David B. MacQueen and Mads Tofte", title = "A Semantics for Higher-order Functors", booktitle = o5 # " " # esop, year = 1994, series = lncs, volume = 788, publisher = springer, pages = "409--423", } @inproceedings{macqueen:modular-struct, author = "David MacQueen", title = "Using Dependent Types to Express Modular Structure", booktitle = o13 # " " # popl, year = 1986, month = jan, pages = "277--286", address = "St.\ Petersburg Beach, Florida", } @inproceedings{maqueen:modules, author = "David MacQueen", title = "Modules for {Standard} {ML}", booktitle = 1984 # " " # lfp, year = 1984, month = aug, address = "Austin, Texas", pages = "198--207", } @InProceedings{maes:reflection, author = {Pattie Maes}, title = {Concepts and experiments in computational reflection}, booktitle = {Proceedings of the 2nd Annual Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA '87), (Orlando, FL)}, pages = {147--155}, year = 1987, month = oct } @inproceedings{martin-lof:constructive-math-and-programming, author = "Per Martin-L{\"{o}}f", title = "Constructive Mathematics and Computer Programming", booktitle = "Sixth International Congress of Logic, Methodology and Philosophy of Science", pages = "153--175", publisher = noholland, year = 1982, series = "Studies in Logic and the Foundations of Mathematics", volume = 104, } @inproceedings{martin-lof:intuitionistic-types-pred, author = "Per Martin-L{\"{o}f}", title = "An Intuitionistic Theory of Types: Predicative Part", booktitle = "Proceedings of the Logic Colloquium, 1973", pages = "73--118", publisher = noholland, year = 1975, series = "Studies in Logic and the Foundations of Mathematics", volume = 80, } @article{meertens:paramorphisms, author = {Lambert G. L. T. Meertens}, title = {Paramorphisms}, journal = {Formal Aspects of Computing}, pages = {413--424}, year = 1992, volume = 4, number = 5, publisher = springer } @inproceedings{mmf91m ,author="Erik Meijer and Fokkinga, Maarten M. and Ross Paterson" ,title="Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" ,booktitle="FPCA91: " # fpca ,pages="124--144" ,year=1991 } % ,volume=523 % ,series=lncs % ,publisher=springer @inproceedings{ meijer95bananas, author = "Erik Meijer and Graham Hutton", title = "Bananas in Space: Extending Fold and Unfold to Exponential Types", booktitle = "FPCA95: " # fpca, month = jun, address = "La Jolla, CA", pages = "324--333", year = 1995, url = "citeseer.nj.nec.com/293490.html" } @article{mendler:inductive-types, author = "Nax Paul Mendler", title = "Inductive Types and Type Constraints in the Second-Order Lambda Calculus", journal = "Annals of Pure and Applied Logic", year = 1991, volume = 51, number = "1--2", pages = "159--172", } @phdthesis{mendler:phd, author = "Paul Francis Mendler", title = "Inductive Definition in Type Theory", school = cornell-cs, month = sep, year = 1987, address = ith-ny, } @inproceedings{meyer+:type-not-type, author = "Albert R. Meyer and Mark B. Reinhold", title = "`{T}ype' is Not a Type", booktitle = o13 # " " # popl, year = 1986, month = jan, pages = "287--295", address = "St. Petersburg Beach, Florida", } @InProceedings{millen92, author = {J. K. Millen}, title = {A Resource Allocation Model for Denial of Service}, booktitle = ieeesp, pages = {137--147}, year = 1992, address = {Oakland, CA}, month = {May}, publisher = {IEEE Computer Society Press} } @InCollection{millen95, author = {Jonathan K. Millen}, title = {Denial of Service: A Perspective}, booktitle = {Dependable Computing for Critical Applications 4}, publisher = springer, year = 1995, editor = {F. Cristian and G. {Le Lann} and T. Lunt}, volume = 9, series = {Dependable Computing and Fault Tolerant Systems}, address = {Wien, Austria} } @book{milner+:sml, title = "The Definition of {S}tandard {ML}", author = "Robin Milner and Mads Tofte and Robert Harper", publisher = mit-press, address = cam-ma, year = 1990, } @book{milner+:sml-comment, title = "Commentary on {S}tandard {ML}", author = "Robin Milner and Mads Tofte", publisher = mit-press, address = cam-ma, year = 1991, } @book{milner+:sml97, title = "The Definition of {Standard} {ML} (Revised)", author = "Robin Milner and Mads Tofte and Robert Harper and David MacQueen", publisher = mit-press, address = cam-ma, year = 1997, } @Article{milner:alg-w, author = {Robin Milner}, title = {A Theory of Type Polymorphism in Programming}, journal = {Journal of Computer and System Sciences }, year = 1978, volume = 17, number = 3, pages = {348--375} } @InProceedings{millstein+:eml, author = {Todd Millstein and Colin Bleckner and Craig Chambers}, title = {Modular Typechecking for Hierarchically Extensible Datatypes and Functions}, booktitle = icfp, year = 2002, address = {Pittsburgh, PA, USA}, month = oct } @inproceedings{minamide+:typed-closure-conversion, author = "Yasuhiko Minamide and Greg Morrisett and Robert Harper", title = "Typed Closure Conversion", pages = "271--283", booktitle = o23 # " " # popl, address = "St. Petersburg, Florida", month = jan, year = 1996, } @unpublished{minamide:full-lift, author = "Yasuhiko Minamide", title = "Full Lifting of Type Parameters", note = "Submitted for publication. Earlier version published as ``Compilation Based on a Calculus for Explicit Type-Passing'' in the {\em Second Fuji International Workshop on Functional and Logic Programming,\/} 1996.", } @InProceedings{minimide99space, author = {Yasuhiko Minamide}, title = {Space-Profiling Semantics of the Call-by-Value Lambda Calculus and the CPS transformation}, booktitle = o3 # " " # hoots, pages = {103--118}, year = 1999, volume = 26, series = {Electronic Notes in Theoretical Computer Science}, address = {http://www.elsevier.nl/locate/entcs}, publisher = {Elsevier} } @book{mips, title = "{MIPS} {RISC} Architecture", author = "Gerry Kane and Joe Heinrich", publisher = "Prentice-Hall", year = 1991, } @article{mitchell+:existential, author = "John C. Mitchell and Gordon D. Plotkin", title = "Abstract Types Have Existential Type", journal = toplas, year = 1988, volume = 10, number = 3, month = jul, pages = "470--502", } @Book{mitchell:book, author = {John C. Mitchell}, title = {Foundations for Programming Languages}, publisher = mit-press, year = 1996 } @article{moggi:computation-monad, author = "Eugenio Moggi", title = "Notions of Computation and Monads", journal = iandc, volume = 93, year = 1991, pages = "55-92", } @INPROCEEDINGS{moreau-Queinnec:DSL97, AUTHOR = {Luc Moreau and Christian Queinnec}, TITLE = {{Design and Semantics of Quantum: a Language to Control Resource Consumption in Distributed Computing}}, BOOKTITLE = {Usenix Conference on Domain-Specific Languages (DSL'97)}, ADDRESS = {Santa-Barbara, California}, YEAR = 1997, PAGES = {183--197}, MONTH = OCT, PS = {http://www.ecs.soton.ac.uk/~lavm/papers/dsl97.ps.gz}, EXPORT = {yes}, PIND = {EZ~02~01~04}, ABSTRACT = {This paper describes the semantics of Quantum, a language that was specifically designed to control resource consumption of distributed computations, such as mobile agent style applications. In Quantum, computations can be driven by mastering their resource consumption. Resources can be understood as processors cycles, geographical expansion, bandwidth or duration of communications, etc. We adopt a generic view by saying that computations need energy to be performed. Quantum relies on three new primitives that deal with energy. The first primitive creates a tank of energy associated with a computation. Asynchronous notifications inform the user of energy exhaustion and computation termination. The other two primitives allow us to implement suspension and resumption of computations by emptying a tank and by supplying more energy to a tank. The semantics takes the form of an abstract machine with explicit parallelism and energy-related primitives.} } @inproceedings{morrisett+:abstract-memory-management, author = "Greg Morrisett and Matthias Felleisen and Robert Harper", title = "Abstract Models of Memory Management", booktitle = "FPCA95: " # fpca, pages = "66--77", year = 1995, month = jun, address = "La Jolla, CA", } @incollection{ morrisett97semantics, author = "Greg Morrisett and Robert Harper", title = "Semantics of Memory Management for Polymorphic Languages", booktitle = "Higher Order Operational Techniques in Semantics", publisher = "Newton Institute, Cambridge University Press", editor = "Andrew Gordon and Andrew M. Pitts", year = "1997", pages = {175--226}, url = "citeseer.nj.nec.com/147455.html" } @inproceedings{morrisett+:poly-memory-management, author = "Greg Morrisett and Robert Harper", title = "Semantics of Memory Management for Polymorphic Languages", editor = "A. D. Gordon and A. M. Pitts", booktitle = "Higher Order Operational Techniques in Semantics", publisher = cambridge-press, year = 1997, } @inproceedings{morrisett+:stal, author = "Greg Morrisett and Karl Crary and Neal Glew and David Walker", title = "Stack-Based Typed Assembly Language", booktitle = o2 # " " # tic, year = 1998, month = mar, series = lncs, volume = 1473, publisher = springer, note = "Extended version published as CMU technical report CMU-CS-98-178.", memo = "Extended version also published as Fox Memorandum CMU-CS-FOX-98-05.", } @article{morrisett+:tal, author = "Greg Morrisett and David Walker and Karl Crary and Neal Glew", title = "From {System} {F} to Typed Assembly Language", journal = toplas, year = 1999, month = may, volume = 21, number = 3, pages = {528--569}, note = "An earlier version appeared in the 1998 Symposium on Principles of Programming Languages.", } @inproceedings{morrisett+:tal-popl, author = "Greg Morrisett and David Walker and Karl Crary and Neal Glew", title = "From {System} {F} to Typed Assembly Language", booktitle = o25 # " " # popl, month = jan, year = 1998, address = "San Diego", pages = "85--97", note = "Extended version published as Cornell University technical report TR97-1651.", } @techreport{morrisett+:tal-tr, author = "Greg Morrisett and David Walker and Karl Crary and Neal Glew", title = "From {System} {F} to Typed Assembly Language (Extended Version)", institution = cornell-cs, year = 1997, month = nov, number = "TR97-1651", } @inproceedings{morrisett+:til-safety, author = "Greg Morrisett and David Tarditi and Perry Cheng and Chris Stone and Robert Harper and Peter Lee", title = "The {TIL/ML} Compiler: Performance and Safety Through Types", booktitle = "Workshop on Compiler Support for Systems Software", year = 1996, month = feb, address = "Tucson" } @phdthesis{morrisett:phd, author = "Greg Morrisett", title = "Compiling with Types", school = cmu-cs, year = 1995, month = dec, address = pgh-pa, } @inproceedings{mycroft:poly-type-schemes, author = "Alan Mycroft", title = "Polymorphic Type Schemes and Recursive Definitions", booktitle = o6 # " " # "International Symposium on Programming", series = lncs, number = 167, pages = "217--228", publisher = springer, month = apr, year = 1984, } @inproceedings{ myers97parameterized, author = "Andrew C. Myers and Joseph A. Bank and Barbara Liskov", title = "Parameterized Types for {Java}", booktitle = "Conference Record of {POPL} '97: The 24th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages", address = "New York, NY", pages = "132--145", year = "1997", url = "citeseer.nj.nec.com/myers97parameterized.html" } %% O %% %% N %% @inproceedings{necula+:safe-extensions, title = "Safe Kernel Extensions Without Run-Time Checking", author = "George Necula and Peter Lee", booktitle = o2 # " " # osdi, year = 1996, month = oct, pages = "229--243", address = "Seattle", } @inproceedings{necula+:touchstone, title = "The Design and Implementation of a Certifying Compiler", author = "George Necula and Peter Lee", booktitle = 1998 # " " # pldi, year = 1998, month = jun, pages = "333--344", address = "Montreal", } @incollection{necula+:untrusted-agents, author = "George Necula and Peter Lee", title = "Safe, Untrusted Agents using Proof-Carrying Code", booktitle = "Special Issue on Mobile Agent Security", publisher = springer, series = lncs, volume = 1419, month = oct, year = 1997, } @inproceedings{necula:pcc, title = "Proof-Carrying Code", author = "George Necula", booktitle = o24 # " " # popl, year = 1997, month = jan, address = "Paris", pages = "106--119", } @PhdThesis{necula:phd, author = {George Necula}, title = {Compiling with Proofs}, school = {Carnegie Mellon University}, year = 1998, address = pittsburgh-pa, month = sep, note = {Technical Report CMU-CS-98-154} } @inproceedings{neubauer01functional_notation, author = {Matthias Neubauer and Peter Thiemann and Martin Gasbichler and Michael Sperber }, title = {A Functional Notation for Functional Dependencies}, booktitle = {Preliminary Proceedings of the 2001 {ACM SIGPLAN} Haskell Workshop ({HW}'2001) Firenze, Italy 2nd September 2001}, year = 2001, editor = {Ralf Hinze}, number = {UU-CS-2001-23}, institution = {Institute of Information and Computing Sciences Utrecht University} } @Book{nielson+:two-level, author = { Flemming Nielson and Hanne Riis Nielson}, title = {Two-Level Functional Languages}, publisher = cambridge-press, year = 1992, volume = 34, series = {Cambridge Tracts in Theoretical Computer Science} } @inproceedings{ocallahan:jvm-types, author = "Robert O'Callahan", title = "A Simple, Comprehensive Type System for {Java} Bytecode Subroutines", booktitle = o26 # " " # popl, year = 1999, month = jan, address = "San Antonio, Texas", pages = {70--78}, } @inproceedings{ odersky96putting, author = "Martin Odersky and Konstantin {L\"aufer}", title = "Putting Type Annotations to Work", booktitle = "Conference Record of {POPL} '96: The 23rd {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages, St. Petersberg Beach, Florida", address = "New York, N.Y.", pages = "54-67", year = "1996", url = "citeseer.nj.nec.com/odersky96putting.html" } @article{ohearn+:param-local-vars, author = "Peter W. O'Hearn and Robert D. Tennent", title = "Parametricity and Local Variables", journal = jacm, volume = 42, number = 3, pages = "658--709", year = 1995, month = may, } @inproceedings{okasaki:catenable-dequeues, author = "Chris Okasaki", title = "Catenable Double-Ended Queues", booktitle = 1997 # " " # icfp, year = 1997, month = jun, address = "Amsterdam", pages = "66--74", } @Book{okasaki:phd, author = {Chris Okasaki}, title = {Purely Functional Data Structures}, publisher = cambridge-press, year = 1998 } @InProceedings{okasaki99fast, author = {Chris Okasaki}, title = {From fast exponentiation to square matrices: An adventure in types}, booktitle = 1999 # " " # icfp, pages = {28--35}, year = 1999, month = sep, address = {Paris, France} } %% P %% @techreport{palmgren+:domain-interp-itt, author = "Erik Palmgren and Viggo Stoltenberg-Hansen", title = "Domain Interpretations of Intuitionistic Type Theory", institution = "Uppsala University, Department of Mathematics", year = 1989, month = jan, type = "{U.U.D.M.} Report", number = "1989:1", } @article{palmgren:infosys-interp-mltt, author = "Erik Palmgren", title = "An Information System Interpretation of {Martin-L\"{o}f}'s Partial Type Theory with Universes", journal = iandc, year = 1993, volume = 106, pages = "26--60", } @inproceedings{palsberg:object-inference, author = "Jens Palsberg", title = "Efficient Inference of Object Types", booktitle = o9 # " " # lics, year = 1994, month = jul, pages = "186--195", address = "Paris", } @article{park:fixpoint, author = "David Park", title = "Fixpoint Induction and Proofs of Program Properties", journal = "Machine Intelligence", volume = 5, year = 1969, pages = "59--78", } @Article{parigot:recursive, author = {Michel Parigot}, title = {Recursive Programming with Proofs}, journal = tcs, year = 1992, volume = 94, number = 2, pages = {335-356}, month = mar } @INPROCEEDINGS{Moh93, author = {Christin Paulin-Mohring}, booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications}, editor = {Marc Bezem and Jan Friso Groote}, institution = {LIP-ENS Lyon}, note = {LIP research report 92-49}, number = {664}, pages ={328--345}, series = {Lecture Notes in Computer Science}, title = {Inductive Definitions in the System {Coq} - Rules and Properties}, type = {research report}, year = {1993}, } @book{paulson:lcf, author = "Lawrence C. Paulson", title = "Logic and Computation: Interactive Proof with {Cambridge} {LCF}", year = 1987, publisher = cambridge-press, } @InProceedings{persson99lctes, author = {Patrik Persson}, title = {Live Memory Analysis for Garbage Collection in Embedded Systems}, booktitle = 1999 # " " # lctes, pages = {45--54}, year = 1999, volume = 34, number = 7, series = {SIGPLAN Notices}, address = {Atlanta, GA}, month = {may} } @TECHREPORT{PetersonHL97, AUTHOR = {Peterson, John and Hudak, Paul and Ling, Gary Shu}, TITLE = {Principled Dynamic Code Improvement}, INSTITUTION = {Department of Computer Science, Yale University}, NUMBER = {YALEU/DCS/RR-1135}, MONTH = {July}, YEAR = {1997}, URL = {http://www.cis.upenn.edu/~mwh/papers_DB/yale-tr.ps} } @Unpublished{peyton-jones:boilerplate, author = {Simon {Peyton Jones} and Ralf Laemmel}, title = {Scrap your Boilerplate: a practical design pattern for generic programming}, note = {Available at http://research.microsoft.com/Users/simonpj/papers/hmap/}, year = 2002 } @InProceedings{peyton-jones+:unboxed, author = {Simon {Peyton Jones} and John Launchbury}, title = {Unboxed values as first class citizens in a non-strict functional programming language}, booktitle = "FPCA91:" # " " # fpca, pages = {636-666}, year = 1991, address = {New York, NY}, month = aug, publisher = {ACM Press} } @inproceedings{peyton-jones+:ghc, author = "Simon L. {Peyton Jones} and Cordelia V. Hall and Kevin Hammond and Will Partain and Philip Wadler", title = "The {G}lasgow {H}askell compiler: a technical overview", year = 1993, month = jul, booktitle = "Proc. UK Joint Framework for Information Technology (JFIT) Technical Conference", } @inproceedings{peyton-jones+:imperative-fnal-prog, author = "Peyton Jones, Simon L. and Philip Wadler", title = "Imperative Functional Programming", booktitle = o20 # " " # popl, address = "Charleston, South Carolina", year = 1993, month = jan, } @TechReport{peyton-jones99:haskell, author = {Simon {Peyton Jones} and John Hughes}, title = {Report on the Programming Language {H}askell 98, A Non-strict Purely Functional Language}, institution = {Yale University, Department of Computer Science}, year = 1999, number = {YALEU/DCS/RR-1106}, month = feb, note = {Available from \url{http://www.haskell.org/definition/}} } @Book{peyton-jones03:haskell, editor = {Simon {Peyton Jones}}, title = {Haskell 98 Language and Libraries: The Revised Report}, publisher = {Cambridge University Press}, year = 2003 } @InProceedings{pfenning+:twelf, author = {Frank Pfenning and Carsten Sch\"urmann}, title = {System description: Twelf---a meta-logical framework for deductive systems}, booktitle = {Proceedings of the 16th International Conference on Automated Deduction (CADE-16)}, pages = {202--206}, year = 1999, editor = {H. Ganzinger}, address = {Trento, Italy}, month = jul } @InProceedings{pfenning+:hoas, author = {Frank Pfenning and Conal Elliott}, title = {Higher-order Abstract Syntax}, booktitle = 1988 # " " # pldi, pages = {199-208}, year = 1988, address = {Atlanta, GA, USA}, month = jun } @inproceedings{pfenning+:leap, author = "Frank Pfenning and Peter Lee", title = "{LEAP}: A language with eval and polymorphism", booktitle = "Proceedings of the International Joint Conference on Theory and Practice in Software Development", address = "Barcelona", year = 1989, series = lncs, volume = 352, publisher = springer, pages = "345--359", } @techreport{pfenning:inductive-types-coq, author = "Frank Pfenning", title = "Inductively Defined Types in the Calculus of Constructions", institution = cmu-cs, month = nov, year = 1988, type = "Ergo Report", number = "88-069", } @INPROCEEDINGS{PfPa89, author = {Frank Pfenning and Christin Paulin-Mohring}, booktitle = {Proceedings of Mathematical Foundations of Programming Semantics}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 442, title = {Inductively defined types in the {Calculus of Constructions}}, year = 1990, pages = {209--228} } @inproceedings{pfenning:partial-inference, author = "Frank Pfenning", title = "Partial Polymorphic Type Inference and Higher-Order Unification", booktitle = 1998 # " " # lfp, year = 1988, month = jul, pages = "153--163", address = "Snowbird, Utah", } @article{pfenning:recon-undecidable, author = "Frank Pfenning", title = "On the Undecidability of Partial Polymorphic Type Reconstruction", journal = "Fundamenta Informaticae", year = 1993, volume = 19, number = "1,2", pages = "185--199", } @inproceedings{pfenning:unification, author = "Frank Pfenning", title = "Unification and Anti-Unification in the Calculus of Constructions", booktitle = o6 # " " # lics, year = 1991, month = jul, pages = "74--85", address = "Amsterdam", } @article{pierce+:ho-subtyping, author = "Benjamin Pierce and Martin Steffen", title = "Higher-Order Subtyping", year = 1997, journal = "Theoretical Computer Science", volume = 176, number = "1--2", pages = "235--282", } @article{pierce+:oop-tt-foundations, author = "Benjamin C. Pierce and David N. Turner", title = "Simple Type-Theoretic Foundations For Object-Oriented Programming", journal = jfp, year = 1994, month = apr, volume = 4, number = 2, pages = "207--247", } @inproceedings{pierce+:oop-wo-rectype, author = "Benjamin C. Pierce and David N. Turner", title = "Object-Oriented Programming Without Recursive Types", booktitle = o20 # " " # popl, year = 1993, month = jan, pages = "299--312", } @techreport{pierce+:programming-in-ho-lambda, author = "Benjamin Pierce and Scott Dietzen and Spiro Michaylov", title = "Programming in Higher-Order Typed Lambda-Calculi", year = 1989, institution = cmu-cs, number = "CMU-CS-89-111", } @incollection{pierce:bq-undecidable, author = "Benjamin C. Pierce", title = "Bounded Quantification is Undecidable", booktitle = "Theoretical Aspects of Object-Oriented Programming", year = 1994, publisher = "The {MIT} Press", pages = "427--459", } @article{pierce:intersection-and-bq, author = "Benjamin C. Pierce", title = "Intersection Types and Bounded Polymorphism", pages = "129--193", journal = mscs, month = apr, year = 1997, volume = 7, number = 2, } @phdthesis{pierce:phd, author = "Benjamin C. Pierce", title = "Programming with Intersection Types and Bounded Polymorphism", school = cmu-cs, year = 1991, month = dec, address = pgh-pa, } @manual{pierce:pict, author = "Benjamin C. Pierce", title = "Programming in the Pi-Calculus: An Experiment in Concurrent Language Design", year = 1995, month = dec, webnote = "Available at http://www.cs.indiana.edu/hyplan/pierce/ftp/pict/Html/Pict.html", } @inproceedings{ pierce98local, author = "Benjamin C. Pierce and David N. Turner", title = "Local Type Inference", booktitle = "Conference Record of {POPL} 98: The 25TH {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages, San Diego, California", address = "New York, NY", pages = "252--265", year = "1998", url = "citeseer.nj.nec.com/pierce98local.html" } @Book{pierce:book, author = {Benjamin C. Pierce}, title = {Types and Programming Languages}, publisher = mit-press, year = 2002 } @InProceedings{pierce+:recursive-types-dummies, author = "Vladimir Gapeyev and Michael Y. Levin and Benjamin C. Pierce", title = "Recursive Subtyping Revealed", booktitle = 2000 # " " # icfp, address = "Montreal", month = sep, year = 2000, pages = {221--232}, url = "citeseer.nj.nec.com/470426.html" } } @inproceedings{ pitts00metalanguage, author = "Andrew M. Pitts and Murdoch Gabbay", title = "A Metalanguage for Programming with Bound Names Modulo Renaming", booktitle = "Mathematics of Program Construction", pages = "230--255", year = "2000", url = "citeseer.nj.nec.com/pitts00metalanguage.html" } @TechReport{plotkin:logical-relations, author = {G.D. Plotkin}, title = {Lambda-definablility and logical relations}, institution = {University of Edinburgh, School of Artificial Intelligence}, year = 1973, number = {SAI-RM-4} } @article{plotkin:name-value, author = "Gordon D. Plotkin", title = "Call-by-name, call-by-value, and the lambda calculus", journal = tcs, volume = 1, year = 1975, pages = "125--159", } @inbook{plotkin:lambda-definability, author = {G.D. Plotkin}, chapter = {Lambda definability in the full type hierarchy}, book = {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, year = 1980, pages = {363--373}, publisher = {Academic Press} } @inproceedings{plotkin+:param-logic, author = "Gordon Plotkin and Mart\'{\i}n Abadi", title = "A Logic for Parametric Polymorphism", booktitle = tlca, year = 1993, pages = "361--375", } @inproceedings{plotkin+:subtype-parametricity, author = "Gordon Plotkin and Mart\'{\i}n Abadi and Luca Cardelli", title = "Subtyping and Parametricity", booktitle = o9 # " " # lics, year = 1994, month = jul, pages = "310--319", } @MastersThesis{poulsen:masters, author = {Eigil Rosager Poulsen}, title = {Representation analysis for efficient implementation of polymorphism}, school = {DIKU, University of Copenhagen}, year = 1993, month = apr } %% Q %% %% R %% @inproceedings{pottier:simp-subtyping, author = "Fran\c{c}ois Pottier", title = "Simplifying Subtyping Constraints", booktitle = 1996 # " " # icfp, year = 1996, month = may, address = "Philadelphia", pages = "122--133", } @inproceedings{reed99:xenoservers, author = "D. Reed and I. Pratt and S. Early and P. Menage and N. Stratford", title = "Xenoservers: Accountable execution of untrusted programs", booktitle = o7 # " " # hotos, month = 1999, year = "1999" } @InProceedings{reistad94, author = {Brian Reistad and David K. Gifford}, title = {Static Dependent Costs for Estimating Execution Time}, booktitle = lfp, pages = {65--78}, year = 1994, address = {Orlando, FL}, month = jul } @inproceedings{remy+:objective-ml, title = "Objective {ML}: A Simple Object-Oriented Extension of {ML}", author = "Didier R\'{e}my and J\'{e}r\^{o}me Vouillon", booktitle = o24 # " " # popl, year = 1997, month = jan, address = "Paris", pages = "40--53", } @inproceedings{remy:ml-art, author = "Didier R\'{e}my", title = "Programming Objects with {ML-ART}: An Extension to {ML} with Abstract and Record Types", booktitle = tacs # " 1994", address = "Sendai, Japan", year = 1994, pages = "321--346", series = lncs, volume = 789, publisher = springer, } @incollection{remy:record-ext, author = "Didier R\'{e}my", title = "Type Inference for Records in a Natural Extension of {ML}", booktitle = "Theoretical Aspects of Object-Oriented Programming", editor = "Carl A. Gunter and John C. Mitchell", chapter = 3, pages = "67--95", year = 1994, publisher = mit-press, address = cam-ma, } @inproceedings{remy:type-rec-var, author = "Didier R\'{e}my", title = "Typechecking Records and Variants in a Natural Extension of {ML}", booktitle = o16 # " " # popl, pages = "77--87", year = 1989, month = jan, } @inproceedings{reppy+:simple-objects, author = "John Reppy and Jon Riecke", title = "Simple Objects for {S}tandard {ML}", booktitle = 1996 # " " # pldi, year = 1996, month = may, pages = "171--180", address = "Philadelphia", } @inproceedings{reynolds:definitional-interp, author = "John C. Reynolds", title = "Definitional Interpreters for Higher-Order Programming Languages", booktitle = "Conference Record of the 25th National ACM Conference", pages = "717--740", address = "Boston", month = aug, year = "1972", } @inproceedings{reynolds:essence-of-algol, author = "John C. Reynolds", title = "The Essence of {Algol}", booktitle = "Proceedings of the International Symposium on Algorithmic Languages", editor = "J. W. de Bakker and J. C. van Vliet", address = "Amsterdam", year = 1981, month = oct, pages = "345--372", publisher = noholland, } @techreport{reynolds:forsythe, author = "John C. Reynolds", title = "Design of the Programming Language {F}orsythe", year = 1996, month = jun, institution = cmu-cs, number = "CMU-CS-94-146", } @incollection{reynolds:implicit-conversions, author = "John C. Reynolds", title = "Using Category Theory to Design Implicit Conversions and Generic Operators", booktitle = "Semantics-Directed Compiler Generation", publisher = springer, series = lncs, volume = 94, year = 1980, pages = "211--258", } @inproceedings{reynolds:intersection-coherence, author = "John C. Reynolds", title = "The Coherence of Languages with Intersection Types", booktitle = tacs # " 1991", address = "Sendai, Japan", year = 1991, pages = "675--700", series = lncs, volume = 526, publisher = springer, } @inproceedings{REYNOLDS83, author = "John C. Reynolds", title = "Types, Abstraction and Parametric Polymorphism", booktitle = "Information Processing '83", year = 1983, pages = "513--523", publisher = noholland, note = "Proceedings of the IFIP 9th World Computer Congress", } @inproceedings{reynolds:polymorphism-not-set-theoretic, author = "John C. Reynolds", title = "Polymorphism is not Set-Theoretic", booktitle = "Proceedings of the International Symposium on Semantics of Data Types", year = 1984, series = lncs, volume = 173, publisher = springer, pages = {145--156} } @inproceedings{reynolds:syntactic-control-interfere, author = "John C. Reynolds", title = "Syntactic Control of Interference", booktitle = o5 # " " # popl, year = 1978, pages = "39--46", address = "Tucson, Arizona", } @inproceedings{reynolds:syntactic-control-interfere2, author = "John C. Reynolds", title = "Syntactic Control of Interference, Part 2", booktitle = o16 # " " # icalp, month = jul, year = 1989, } @inproceedings{reynolds:type-structure, author = "John C. Reynolds", title = "Towards a theory of type structure", booktitle = "Programming Symposium", pages = "408--425", series = lncs, volume = 19, year = 1974, } @Article{reynolds+:funept, author = {John C.~Reynolds and Gordon D.~Plotkin}, title = {On Functors Expressible in the Polymorphic Typed Lambda Calculus}, journal = {Information and Computation}, year = 1993, volume = 105, pages = {1--29} } @techreport{rezus:semant-ctt, author = "Adrian Rezus", title = "Semantics of Constructive Type Theory", institution = "Informatics Department, Faculty of Science, Nijmegen, University, The Netherlands", year = 1985, month = sep, number = 70, } @inproceedings{ roe97lightweight, author = "Paul Roe and Clemens Szyperski", title = "Lightweight Parametric Polymorphism for Oberon", booktitle = "Proc. of Joint Modular Languages Conference ({JMLC})", address = "Linz, Austria", year = "1997", url = "citeseer.nj.nec.com/roe97lightweight.html" } @INPROCEEDINGS{Rouaix96, AUTHOR = {Fran\c{c}ois Rouaix}, TITLE = {A {Web} navigator with applets in {Caml}}, BOOKTITLE = {Proceedings of the 5th International {World} {Wide} {Web} Conference, in {Computer} {Networks} and {Telecommunications} {Networking}}, VOLUME = {28}, YEAR = {1996}, PUBLISHER = {Elsevier}, MONTH = {May}, PAGES = {1365--1371}, URL = {http://pauillac.inria.fr/~rouaix/mmm/papers/mmm.ps.gz} } @InProceedings{ ruehr98structural, author = "Fritz Ruehr", title = "Structural polymorphism", booktitle = "Informal Proceedings Workshop on Generic Programming, WGP'98, Marstrand, Sweden, 18 June 1998.", editor = "Roland Backhouse and Tim Sheard", year = 1998, url = "citeseer.nj.nec.com/ruehr98structural.html" } @PhdThesis{ruehr:phd, author = {Fritz Ruehr}, title = {Analytical and Structural Polymorphism Expressed Using Patterns Over Types}, school = {University of Michigan}, year = 1992 } @inproceedings{ruf:df, title = "Partitioning Dataflow Analyses Using Types", author = "Erik Ruf", booktitle = o24 # " " # popl, year = "1997", month = jan, pages = "15--26", address = "Paris", } @article{russell:types, author = "Bertrand Russell", title = "Mathematical logic as based on a theory of type", journal = "Am. J. Math.", volume = 30, pages = "222--262", year = 1908, } %% S %% @inproceedings{saha+:type-lift, author = "Bratin Saha and Zhong Shao", title = "Optimal Type Lifting", booktitle = o2 # " " # tic, year = 1998, month = mar, } @InProceedings{saha+:fully, author = {Valery Trifonov and Bratin Saha and Zhong Shao}, title = {Fully Reflexive Intensional Type Analysis}, booktitle = o5 # " " # icfp, year = 2000, address = "Montreal", month = sep, pages = "82--93", annote = {Extended version is YALEU/DCS/TR-1194} } @InProceedings{saha+:fully-erasure, author = {Bratin Saha and Valery Trifonov and Zhong Shao}, title = {Fully Reflexive Intensional Type Analysis in Type Erasure Semantics}, booktitle = o3 # " " # tic, year = 2000, address = "Montreal", month = sep } @inproceedings{DBLP:conf/types/BradyMM03, author = {Edwin Brady and Conor McBride and James McKinna}, title = {Inductive Families Need Not Store Their Indices}, booktitle = {TYPES}, year = {2003}, pages = {115-129}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3085{\&}spage=115}, crossref = {DBLP:conf/types/2003}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/types/2003, editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani}, title = {Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers}, booktitle = {TYPES}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3085}, year = {2004}, bibsource = {DBLP, http://dblp.uni-trier.de} } @STRING{fossacs11="Foundations of Software Science and Computational Structures, 14th International Conference, FOSSACS 2011, Saarbrucken, Germany"} @InProceedings{abel:fossacs11, author = {Andreas Abel}, title = {Irrelevance in Type Theory with a Heterogeneous Equality Judgement}, optcrossref = {}, optkey = {}, booktitle = fossacs11, optpages = {}, year = {2011}, opteditor = {}, optvolume = {}, optnumber = {}, optseries = {}, optaddress = {}, optmonth = {}, optorganization={}, optpublisher = {}, note = {To appear.}, opturl = {}, optpostscript = {}, optpdf = {}, optdvi = {}, optabstract = {} } @inproceedings{bengtson+:f7, author = {Bengtson, Jesper and Bhargavan, Karthikeyan and Fournet, C\'{e}dric and Gordon, Andrew D. and Maffeis, Sergio}, title = {Refinement Types for Secure Implementations}, booktitle = {Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium}, year = {2008}, isbn = {978-0-7695-3182-3}, pages = {17--32}, numpages = {16}, publisher = {IEEE Computer Society}, address = {Washington, DC, USA}, } @inproceedings{Borgstrom:2011:VSP:1929529.1929532, author = {Borgstrom, Johannes and Chen, Juan and Swamy, Nikhil}, title = {Verifying stateful programs with substructural state and hoare types}, booktitle = {Proceedings of the 5th ACM workshop on Programming languages meets program verification}, series = {PLPV '11}, year = {2011}, isbn = {978-1-4503-0487-0}, location = {Austin, Texas, USA}, pages = {15--26}, numpages = {12}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {affine types, dependent types, security type systems}} @incollection {mishra:erasure, author = {Mishra-Linger, Nathan and Sheard, Tim}, affiliation = {Portland State University}, title = {Erasure and Polymorphism in Pure Type Systems}, booktitle = {Foundations of Software Science and Computational Structures}, series = {Lecture Notes in Computer Science}, editor = {Amadio, Roberto}, publisher = {Springer Berlin / Heidelberg}, isbn = {}, pages = {350-364}, volume = {4962}, year = {2008} } @Article{saltzer75protection, author = "J.H. Saltzer and M.D. Schroeder", title = "The Protection of Information in Computer Systems", journal = {Proceedings of the IEEE}, year = 1975, volume = 63, number = 9, pages = {1278--1308}, month = sep } @article{ schneider00enforceable, author = "Fred B. Schneider", title = "Enforceable security policies", journal = "Information and System Security", volume = "3", number = "1", pages = "30-50", year = "2000", url = "citeseer.nj.nec.com/article/schneider98enforceable.html" } @Article{schurmann:hoas, author = {Carsten Sch\"{u}rmann and Jo\"{e}lle Despeyroux and Frank Pfenning}, title = {Primitive recursion for higher-order abstract syntax}, journal = {Theoretical Computer Science}, year = 2001, volume = 266, number = {1--2}, pages = {1--58}, month = sep } @Unpublished{schuermann:delphin, author = {Carsten Sch\"{u}rmann and Richard Fontana and Yu Liao}, title = {Delphin: Functional Programming with deductive systems}, note = {Available at \url{http://cs-www.cs.yale.edu/homes/carsten/}}, year = 2002 } @inproceedings{scott:advice-modal, author = {Dana Scott}, editor = {K. Lambert}, booktitle = {Philosophical Problems in Logic}, title = {Advice on Modal Logic}, publisher = {D. Riedel Publishing Company}, year = 1973, pages = {143--173} } @inproceedings{scott+:semantics, author = "Dana Scott and Christopher Strachey", title = "Toward a Mathematical Semantics for Computer Languages", booktitle = "Proceedings of the Symposium on Computers and Automata", series = "Microwave Research Institute Symposia Series", volume = 21, publisher = "Polytechnic Institute of Brooklyn", year = 1971, } @inproceedings{scott:lattice-models, author = "Dana Scott", title = "Lattice Theoretic Models for Various Type-Free Calculi", booktitle = "Fourth International Congress of Logic, Methodology and Philosophy of Science", publisher = noholland, year = 1972, } @inproceedings{scott:math-thy-comp, author = "Dana Scott", title = "Outline of a Mathematical Theory of Computation", booktitle = "Fourth Princeton Conference on Information Sciences and Systems", year = 1970, pages = "169--176", } @InProceedings{seltzer96vino, author = {Margo Seltzer and Yasuhiro Endo and Chris Small and Keith Smith}, title = {Dealing with Disaster: Surviving Misbehaved Kernel Extensions}, booktitle = o2 # " " # osdi, pages = {213--227}, year = 1996, address = {Seattle, WA}, month = oct } @inproceedings{senizergues:dpda, author = "G\'{e}raud S\'{e}nizergues", title = "The Equivalence Problem for Deterministic Pushdown Automata is Decidable", booktitle = o24 # " " # icalp, year = 1997, month = jul, address = "Bologna, Italy", pages = "671--681", series = lncs, volume = 1256, publisher = springer, } @Book{dylan:manual, author = {Andrew Shalit and David Moon and Orca Starbuck}, title = {The Dylan Reference Manual : The Definitive Guide to the New Object-Oriented Dynamic Language }, publisher = {Apple Press}, year = 1996 } @InProceedings{shao98implementing, author = {Zhong Shao and Christopher League and Stefan Monnier}, title = {Implementing Typed Intermediate Languages}, booktitle = 1998 # " " # icfp, pages = {313--323}, year = 1998, volume = 34, number = 1, series = {{ACM} {SIGPLAN} Notices}, address = {Baltimore, Maryland}, month = {sep} } @inproceedings{shao:flint, author = "Zhong Shao", title = "An Overview of the {FLINT/ML} Compiler", booktitle = 1997 # " " # tic, month = jun, year = 1997, address = "Amsterdam", note = "Published as {B}oston {C}ollege Computer Science Department Technical Report BCCS-97-03", } @inproceedings{shao:rep-analysis, author = "Zhong Shao", title = "Flexible Representation Analysis", booktitle = 1997 # " " # icfp, year = 1997, month = jun, address = "Amsterdam", pages = "85--98", } @inproceedings{shao:typed-module-comp, author = "Zhong Shao", title = "Typed Cross-Module Compilation", booktitle = 1998 # " " # icfp, year = 1998, month = sep, address = "Baltimore, Maryland", pages = "141--152", } @Article{shaw89time, author = {Alan C. Shaw}, title = {Reasoning about Time in Higher-Level Language Software}, journal = tse, year = 1989, volume = 15, number = 7, pages = {875--889}, month = jul } @TechReport{ sheard93type, author = "Tim Sheard", title = "Type parametric programming", number = "CSE 93-018", institution = {Oregon Graduate Institute}, year = 1993, url = "citeseer.nj.nec.com/sheard93type.html" } @inproceedings{shields01object-oriented, author = {Mark Shields and Simon {Peyton Jones}}, title = {Object-Oriented Style Overloading for Haskell}, booktitle = {Electronic Notes in Theoretical Computer Science}, volume = {59}, issue = {1}, publisher = {Elsevier Science Publishers}, editor = {Nick Benton and Andrew Kennedy}, year = {2001}, url = "http://www.elsevier.com/gej-ng/31/29/23/89/27/show/Products/notes/index.htt#008" } @Article{shostak:residue, author = {R. Shostak}, title = {Deciding linear inequalities by computing loop residues}, journal = jacm, year = 1981, volume = 28, number = 4, pages = {748--752}, month = oct } @inproceedings{sirer+:spinlink, author = "Emin Gun Sirer and Marc E. Fiuczynski and Przemyslaw Pardyak and Brian N. Bershad", title = "Safe Dynamic Linking in an Extensible Operating System", booktitle = o1 # " " # wcsss, year = 1996, month = "February", address = "Tucson", } @InProceedings{smith00alias, author = {Frederick Smith and David Walker and Greg Morrisett}, title = {Alias Types}, booktitle = {European Symposium on Programming}, year = 2000, address = {Berlin, Germany}, month = mar } @phdthesis{smithg:phd, author = "Geoffrey Seward Smith", title = "Polymorphic Type Inference For Languages with Overloading and Subtyping", school = cornell-cs, year = 1991, month = aug, address = ith-ny, } @Article{smith+:active, author = {Jonathan M. Smith and Kenneth L. Calvert and Sandra L. Murphy and Hilarie K. Orman and Larry L. Peterson}, title = {Activating networks: A progress report}, journal = {IEEE Computer}, year = {1999}, OPTkey = {}, OPTvolume = {32}, OPTnumber = {4}, OPTpages = {32--41}, OPTmonth = apr, OPTnote = {}, OPTannote = {} } @article{smith:partial-total, author = "Scott F. Smith", title = "Hybrid Partial-Total Type Theory", journal = "International Journal of Foundations of Computer Science", volume = 6, pages = "235--263", year = 1995, } @phdthesis{smith:phd, author = "Scott Fraser Smith", title = "Partial Objects in Type Theory", school = cornell-cs, month = jan, year = 1989, address = ith-ny, } @InProceedings{smith:reflection, author = {Brian Cantwell Smith}, title = {Reflection and Semantics in {LISP}}, booktitle = o14 # " " # popl, pages = {23--35}, year = 1984 } @inproceedings{solomon:type-defs-param, author = "Marvin Solomon", title = "Type Definitions with Parameters (Extended Abstract)", booktitle = o5 # " " # popl, year = 1978, month = jan, address = "Tucson, Arizona", pages = "31--38", } @InProceedings{spatscheck99:_defen_scout, author = {Oliver Spatscheck and Larry L.Peterson }, title = {Defending against denial of service attacks in Scout}, booktitle = o3 # " " # sosp, pages = {59-72}, year = 1999 } @InProceedings{splawski+:type-fixpoints, author = {Zdzis\l{}aw Sp\l{}awski and Pawe\l{} Urzyczyn}, title = {Type Fixpoints: Iteration vs. Recursion}, booktitle = o4 # " " # icfp, pages = {102--113}, year = 1999, address = {Paris, France}, month = sep } @TechReport{spoonhower98telephony, author = {Daniel Spoonhower and Grzegorz Czajkowski and Chris Hawblitzel and Chi-Chao Chang and Deyu Hu and Thorsten von Eicken}, title = {Design and Evaluation of an Extensible Web & Telephony Server based on the J-Kernel}, institution = cornell-cs, year = 1998, number = {TR98-1715}, address = {ithaca-ny} } @inproceedings{stansifer:subtype-inf, title = "Type Inference with Subtypes", author = "Ryan Stansifer", booktitle = o15 # " " # popl, address = "San Diego", year = 1988, month = jan, pages = "88--97", } @Article{statman:logical-relations, author = {R. Statman}, title = {Logical Relations and Typed Lambda Calculus}, journal = {Information and Control}, year = 1985, volume = 65, pages = {85--97} } @mastersthesis{steele:rabbit, author = "Guy L. {Steele Jr.}", title = "{R}abbit: A Compiler for {S}cheme", school = "MIT", year = 1978, } @Book{steele:cltl2, author = {Guy L. {Steele Jr.}}, title = {Common Lisp the Language, 2nd Edition}, publisher = {Digital Press}, year = 1990 } @techreport{stone+:sml96, title = "A Type-Theoretic Account of {S}tandard {ML} 1996", author = "Chris Stone and Robert Harper", institution = cmu-cs, year = 1996, number = "CMU-CS-96-136", } @InProceedings{stone+:singleton-kinds, author = {Chris Stone and Robert Harper}, title = {Deciding Type Equivalence in a Language with Singleton Kinds}, booktitle = o27 # " " # popl, pages = {214--225}, year = 2000, address = {Boston, MA, USA}, month = jan } @Article{strachey:param, author = {Christopher Strachey}, title = {Fundamental Concepts in Programming Languages}, journal = {Higher-Order and Symbolic Computation}, year = 2000, volume = 13, pages = {11--49}, note = {This paper forms the substance of a course of lectures given at the International Summer School in Computer Programming at Copenhagen in August, 1967.} } @Book{stroustrup:c++, author = {Bjarne Stroustrup}, title = {The C++ Programming Language (Third Edition) }, publisher = {Addison Wesley Longman}, year = 1997, address = {Reading, MA} } @Article{sumii01:hybrid-pe, author = {Eijiro Sumii and Naoki Kobayashi}, title = {A Hybrid Approach to Online and Offline Partial Evaluation}, journal = {Higher-Order and Symbolic Computation}, year = 2001, volume = 14, number = {2/3}, pages = {101--142} } %% T %% @Article{tait:intensional, author = {William W. Tait}, title = {Intensional interpretation of functionals of finite type}, journal = {Journal of Symbolic Logic}, year = 1967, volume = 32, pages = {198--212} } @inproceedings{tarditi+:til, author = "David Tarditi and Greg Morrisett and Perry Cheng and Chris Stone and Robert Harper and Peter Lee", title = "{TIL}: A Type-Directed Optimizing Compiler for {ML}", booktitle = 1996 # " " # pldi, year = 1996, month = may, pages = "181--192", } @PhdThesis{tarditi:phd, author = {David Tarditi}, title = {Design and Implementation of Code Optimizations for a Type-Directed Compiler for Standard ML}, school = {Carnegie Mellon School of Computer Science}, year = 1996, note = {Available as CMU-CS-97-108} } @Article{talpin+:type-effect, author = {J.-P. Talpin and P. Jouvelot}, title = {The Type and Effect Discipline}, journal = {Information and Computation}, year = 1994, volume = 111, number = 2, pages = {245--296} } @Article{tennenhouse97survey, author = "D. Tennenhouse and J. Smith and W. Sincoskie and D. Wetherall and G. Minden", title = "A Survey of Active Network Research", booktitle = {IEEE Communications Magazine}, pages = {80--86}, month = jan, volume = 35, number = 1, year = 1997 } @article{ tennenhouse96towards, author = "David L. Tennenhouse and David J. Wetherall", title = "Towards an Active Network Architecture", journal = "Computer Communication Review", volume = "26", number = "2", year = "1996", pages = "5--18", url = "citeseer.nj.nec.com/tennenhouse96towards.html" } @InProceedings{thiemann01, author = { Peter Thiemann}, title = { Enforcing Security Properties by Type Specialization }, booktitle = { European Symposium on Programming (ESOP'01) }, year = 2001, volume = 2028, series = lncs, address = {Genova, Italy }, month = apr, publisher = {Springer-Verlag} } @InProceedings{tuiryn:subtyping-undecidable, author = {Jerzy Tiuryn and Pawel Urzyczyn}, title = { The subtyping problem for second-order types is undecidable.}, booktitle = {Proceedings of the IEEE Symposion on Logic in Computer Science (LICS 96)}, pages = {74--85}, year = 1996, address = {New Brunswick, New Jersey}, publisher = {IEEE Computer Society Press} } @inproceedings{tofte:higher-order-modules, author = "Mads Tofte", title = "Principal Signatures for Higher-Order Program Modules", booktitle = o19 # " " # popl, year = 1992, month = jan, pages = "189--199", } @article{tofte:polymorphic-refs, author = "Mads Tofte", title = "Type Inference for Polymorphic References", journal = iandc, volume = 89, pages = "1--34", year = 1990, month = nov, } @inproceedings{tolmach:tagless-gc, author = "Andrew Tolmach", title = "Tag-Free Garbage Collection Using Explicit Type Parameters", booktitle = 1994 # " " # lfp, month = jun, pages = "1--11", year = 1994, address = "Orlando" } @InProceedings{vanderwaart+:datatypes, author = {Joseph C. Vanderwaart and Derek Dreyer and Leaf Petersen and Karl Crary and Robert Harper and Perry Cheng}, title = {Typed Compilation of Recursive Datatypes}, booktitle = {{ACM} {SIGPLAN} Workshop on Types in Language Design and Implementation}, year = 2003, address = {New Orleans, USA}, month = jan } %% U %% %% V %% @techreport{van-renesse+:horus, author = "Robbert van Renesse and Takako M. Hickey and Kenneth P. Birman", title = "Design and Performance of {H}orus: A Lightweight Group Communications System", institution = cornell-cs, year = 1994, month = aug, number = "TR 94-1442", } @MastersThesis{vestin:polytypic-ga, author = {M\o{a}ns Vestin}, title = {Genetic algorithms in {H}askell with polytypic programming}, school = {G\"{o}teborg University}, year = 1997 } @inproceedings{viswanathan:fully-abstract-objs, author = "Ramesh Viswanathan", title = "Full Abstraction for First-Order Objects with Recursive Types and Subtyping", booktitle = o13 # " " # lics, year = 1998, month = jun, address = "Indianapolis", } %% W %% @InProceedings{wadler+:type-classes, author = {Philip Wadler and Stephen Blott}, title = {How to make Ad-hoc Polymorphism less ad-hoc}, booktitle = o16 # " " # popl, pages = {60--76}, year = 1989, publisher = {ACM Press} } @inproceedings{wadler:comprehending-monads, author = "Philip Wadler", title = "Comprehending Monads", year = 1992, booktitle = "Mathematical Structures in Computer Science", volume = 2, pages = "461--493", publisher = cambridge-press, } @inproceedings{wadler:effects-to-monads, author = "Philip Wadler", title = "The Marriage of Effects and Monads", booktitle = 1998 # " " # icfp, year = 1998, month = sep, address = "Baltimore", pages = "63--74" } @inproceedings{wadler:fnal-essence, author = "Philip Wadler", title = "The Essence of Functional Programming", booktitle = o19 # " " # popl, year = 1992, month = jan, address = "Albuquerque, New Mexico", } @inproceedings{Wadler89, author = "Philip Wadler", title = "Theorems for Free!", booktitle = "FPCA89:" # " " # fpca, year = 1989, month = sep, pages = "347--359", address = "London", } @inproceedings{wadler:linear-taste, author = "Philip Wadler", title = "A taste of linear logic", booktitle = "Mathematical Foundations of Computer Science", year = 1993, publisher = springer, volume = 711, series = lncs, } @inproceedings{wadler:linear-world, author = "Philip Wadler", title = "Linear types can change the world!", booktitle = "IFIP Working Conference on Programming Concepts and Methods", address = "Sea of Galilee, Israel", month = apr, year = 1990, publisher = noholland, } @inproceedings{wahbe+:sfi, title = "Efficient Software-Based Fault Isolation", author = "Robert Wahbe and Steven Lucco and Thomas Anderson and Susan Graham", booktitle = o14 # " " # sosp, year = 1993, month = dec, pages = "203--216", address = "Asheville", } @TechReport{walker00recursive-alias, author = {David Walker and Greg Morrisett}, title = {Alias Types for Recursive Data Structures}, institution = cornell-cs, year = 2000, number = {TR2000-1787}, address = ith-ny, month = mar, note = {submitted for publication} } @InProceedings{walker00, author = {David Walker}, title = {A Type System for Expressive Security Policies}, booktitle = {Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages January 19 - 21, 2000, Boston, MA USA}, pages = {254--267}, year = 2000, publisher = {ACM Press} } @InProceedings{watanabe+:reflection-oo, author = {Takuo Watanabe and Akinori Yonezawa}, title = {Reflection in an Object-Oriented Concurrent Language}, booktitle = oopsla, pages = {306--315}, year = 1988 } @inproceedings{wand:hoal, author = "Mitchell Wand", title = "Correctness of Procedure Representations in Higher-Order Assembly Language", booktitle = mfps, year = 1991, volume = 598, publisher = springer, series = 1992, pages = "294--311", } @TechReport{washburn+:itaname-tr, author = {Geoffrey Washburn and Stephanie Weirich}, title = {Unifying nominal and structural ad-hoc polymorphism (Extended version)}, institution = {University of Pennsylvania}, year = 2004, note = { Available at \url{http://www.cis.upenn.edu/~sweirich/} } } @Article{wells:typability, author = {Joe B. Wells}, title = {Typability and type checking in System {F} are equivalent and undecidable}, journal = {Ann. Pure Appl. Logic}, year = 1999, volume = 98, number = {1--3}, pages = {111--156} } @book{whitehead+:principia, author = "Alfred North Whitehead and Bertrand Russell", title = "Principia Mathematica", publisher = cambridge-press, year = "1910", edition = "2nd", } @InProceedings{wickline98rtcg, author = {Philip Wickline and Peter Lee and Frank Pfenning}, title = {Run-time Code Generation and Modal-{ML}}, booktitle = 1998 # " " # pldi, pages = {224--235}, year = 1998, month = jun, organization = {ACM SIGPLAN} } @article{wright+:syntactic-soundness, author = "Andrew K. Wright and Matthias Felleisen", title = "A Syntactic Approach to Type Soundness", journal = iandc, volume = 115, pages = "38--94", year = 1994, } @article{wright:value-restriction, author = "Andrew K. Wright", title = "Simple Imperative Polymorphism", journal = "Lisp and Symbolic Computation", volume = 8, number = 4, month = dec, year = 1995, pages = "343--356", } %% X %% @inproceedings{xi+:dependent-types-practical, author = "Hongwei Xi and Frank Pfenning", title = "Dependent Types in Practical Programming", booktitle = o26 # " " # popl, address = "San Antonio, Texas", month = jan, year = 1999, pages = "214--227", } @PhdThesis{xi:phd, author = {Hongwei Xi}, title = {Dependent Types in Practical Programming}, school = {Carnegie Mellon University}, year = 1998, address = {Pittsburgh, PA}, month = sep } @InProceedings{xi+:guarded-datatype, author = {Hongwei Xi and Chiyan Chen and Gang Chen}, title = {Guarded Recursive Datatype Constructors}, booktitle = o30 # " " # popl, pages = {224--235}, year = 2003, address = {New Orleans, LA, USA}, month = jan } %% Y %% @InProceedings{yang:encoding_types, author = {Zhe Yang}, title = {Encoding Types in {ML}-like languages}, booktitle = 1998 # " " # icfp, year = 1998, volume = 34, series = {{ACM} {SIGPLAN} Notices}, address = {Baltimore, MD}, month = sep, pages = { 289--300 } } @inproceedings{ zenger01extensible, author = {Matthias Zenger and Martin Odersky}, title = {Extensible Algebraic Datatypes with Defaults}, year = 2001, month = "September", booktitle = "Proceedings of the International Conference on Functional Programming", address = {Firenze, Italy}, url = {citeseer.nj.nec.com/zenger01extensible.html} } %% Z %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @inproceedings{nanevski:namenec, author = {Aleksandar Nanevski}, title = {Meta-programming with names and necessity}, booktitle = {Proceedings of the seventh ACM SIGPLAN international conference on Functional programming}, year = {2002}, isbn = {1-58113-487-8}, pages = {206--217}, location = {Pittsburgh, PA, USA}, doi = {http://doi.acm.org/10.1145/581478.581498}, publisher = {ACM Press}, } @inproceedings{loh+:dependgen, author = {Andres L\"oh and Dave Clarke and Johan Jeuring}, title = {Dependency-style Generic Haskell}, booktitle = proc # o8 # icfp, year = 2003, pages = {141-152}, location = {Uppsala, Sweden}, } @inproceedings{nanevsk:dynamic, author = {Aleksandar Nanevski}, title = {From dynamic binding to state via modal possibility}, booktitle = {Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming}, year = {2003}, isbn = {1-58113-705-2}, pages = {207--218}, location = {Uppsala, Sweden}, doi = {http://doi.acm.org/10.1145/888251.888271}, publisher = {ACM Press}, } @inproceedings{ambler+:hybrid, author = {Simon Ambler and Roy L. Crole and Alberto Momigliano}, title = {Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction}, booktitle = {Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 2410, year = 2002, isbn = {3-540-44039-9}, } @Unpublished{washburn:modal-spec, author = {Geoffrey Washburn}, title = {Modal Typing for Specifying Run-time Code Generation}, note = {Available from \url{http://www.cis.upenn.edu/~geoffw/research/}}, year = {2001} } @inproceedings{acar+:selective-mem, author = "Umut Acar and Guy Blelloch and Robert Harper", title = "Selective Memoization", booktitle = o30 # " " # popl, year = 2002, month = jan, address = "New Orleans, LA", } @InProceedings{miller:mllam, author = {Dale Miller}, title = {An Extension to {ML} to Handle Bound Variables in Data Structures: Preliminary Report}, booktitle = {Proceedings of the Logical Frameworks BRA Workshop}, year = 1990, month = may } @article{dp:modal-logic-comp, author = "Rowan Davies and Frank Pfenning", title = "A Modal Analysis of Staged Computation", journal = jacm, year = 2001, volume = 48, number = 3, month = "May", pages = "555--604", } @inproceedings{pitts:fresh, author = {Andrew M. Pitts}, title = {A fresh approach to representing syntax with static binders in functional programming}, booktitle = {Proceedings of the sixth ACM SIGPLAN international conference on Functional programming}, year = {2001}, isbn = {1-58113-415-0}, pages = {1--1}, location = {Florence, Italy}, doi = {http://doi.acm.org/10.1145/507635.507637}, publisher = {ACM Press}, } @Unpublished{weirich:type-erasure, author = {Stephanie Weirich}, title = {Higher-Order Intensional Type Analysis in Type-Erasure Semantics}, note = {Available from \url{http://www.cis.upenn.edu/~sweirich/}}, year = 2003 } @inproceedings{lammel:boilerplate, author = {Ralf L\"ammel and Simon {Peyton Jones}}, title = "Scrap your boilerplate: a practical design pattern for generic programming", year = "2003", booktitle = "Proc.\ of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI~2003)" } @inproceedings{dreyer+:modules, author = {Derek Dreyer and Karl Crary and Robert Harper}, title = {A type system for higher-order modules}, booktitle = proc # o30 # popl, year = {2003}, isbn = {1-58113-628-5}, pages = {236--249}, location = {New Orleans, Louisiana, USA}, doi = {http://doi.acm.org/10.1145/604131.604151}, publisher = {ACM Press}, } @InProceedings{Leifer:2003:GAS, author = "James J. Leifer and Gilles Peskine and Peter Sewell and Keith Wansbrough", title = "Global abstraction-safe marshalling with hash types", booktitle = proc # o8 # icfp, year = "2003", pages = "87--98", address = "Uppsala, Sweden" } @TechReport{washburn+:mtr, author = {Geoff Washburn and Stephanie Weirich}, title = {Unifying nominal and structural ad-hoc polymorphism}, institution = {University of Pennsylvania}, year = 2003, note = {Available from \url{http://www.cis.upenn.edu/\~\ washburn/research/}} } @inproceedings{Remy:popl89, author = "Didier Remy", title = "Records and Variants as a natural Extension of {ML}", booktitle = "Sixteenth Annual Symposium on Principles Of Programming Languages", year = 1989, note = "Available from \url{http://doi.acm.org/10.1145/75277.75284}", } @TechReport{vytiniotis+:mtr, author = {Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich}, title = {An Open and Shut Typecase}, institution = {University of Pennsylvania}, year = {2004}, number = {MS-CIS-04-26}, note = {Available from \url{http://www.cis.upenn.edu/~dimitriv/itaname}} } @TechReport{zenger+:expression, author = {Matthias Zenger and Martin Odersky.}, title = {Independently Extensible Solutions to the Expression Problem}, institution = {EPFL Lausanne, Switzerland}, year = 2004, number = {IC/2004/33} } @Book{Nipkow-Paulson-Wenzel:2002, author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, publisher = {Springer}, series = {LNCS}, volume = 2283, year = 2002} @inproceedings{mellies:rectypes, author = {Paul-Andr\'{e} Melli\`{e}s and J\'{e}r\^{o}me Vouillon}, title = {Recursive Polymorphic Types and Parametricity in an Operational Framework}, booktitle = {LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05)}, year = {2005}, isbn = {0-7695-2266-1}, pages = {82--91}, doi = {http://dx.doi.org/10.1109/LICS.2005.42}, publisher = {IEEE Computer Society}, address = {Washington, DC, USA}, } @inproceedings{DBLP:conf/esop/Ahmed06, author = {Amal J. Ahmed}, title = {Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types.}, booktitle = {ESOP}, year = {2006}, pages = {69-83}, ee = {http://dx.doi.org/10.1007/11693024_6}, crossref = {DBLP:conf/esop/2006}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/esop/2006, editor = {Peter Sestoft}, title = {Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings}, booktitle = {ESOP}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3924}, year = {2006}, isbn = {3-540-33095-X}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{appel01:indexed, author = {Andrew W. Appel and David McAllester}, title = {An indexed model of recursive types for foundational proof-carrying code}, journal = {ACM Trans. Program. Lang. Syst.}, volume = {23}, number = {5}, year = {2001}, issn = {0164-0925}, pages = {657--683}, doi = {http://doi.acm.org/10.1145/504709.504712}, publisher = {ACM Press}, address = {New York, NY, USA}, } @Article{johann:higher-order-poly, author = {Patricia Johann}, title = {On Proving the Correctness of Program Transformations based on Free Theorems for Higher-Order Polymorphic Lambda Calculi}, journal = {Math. Struct. Comp. Sci.}, year = 2005, number = 15, pages = {201--229} } @inproceedings{johann04:seq, author = {Johann, Patricia and Voigtl\"{a}nder, Janis}, title = {Free theorems in the presence of seq}, booktitle = {POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, year = {2004}, isbn = {1-58113-729-X}, pages = {99--110}, location = {Venice, Italy}, doi = {http://doi.acm.org/10.1145/964001.964010}, publisher = {ACM}, address = {New York, NY, USA}, } @InCollection{PittsAM:typor, author = {A. M. Pitts}, title = {Typed Operational Reasoning}, booktitle = {Advanced Topics in Types and Programming Languages}, pages = {245--289}, publisher = {The MIT Press}, year = 2005, editor = {B. C. Pierce}, chapter = 7, isbn = {0-262-16228-8} } @techreport{simonet-pottier:gadt-inference, AUTHOR = {Vincent Simonet and Fran\c{c}ois Pottier}, TITLE = {Constraint-Based Type Inference with Guarded Algebraic Data Types}, URL = {http://pauillac.inria.fr/~fpottier/publis/simonet-pottier-hmg.ps.gz}, institution = {INRIA}, MONTH = JUL, YEAR = {2003} } @ARTICLE{simonet-pottier-hmg-toplas, AUTHOR = {Vincent Simonet and Francois Pottier}, TITLE = {A Constraint-Based Approach to Guarded Algebraic Data Types}, MONTH = JAN, YEAR = {2007}, JOURNAL = {ACM Transactions on Programming Languages and Systems}, VOLUME = {29}, NUMBER = {1}, } @article{ Pitts00, author = "Andrew M. Pitts", title = "Parametric polymorphism and operational equivalence", journal = "Mathematical Structures in Computer Science", volume = 10, pages = "321--359", year = "2000" } @techreport{sulzmann+:eadts, author = "Martin Sulzmann and Jeremy Wazny and Peter Stuckey", title = "A framework for extended algebraic data types", year = 2005, institution = "National University of Singapore", keywords = "GADT, type classes" } @inproceedings{spj+:gadt, author = {Simon {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn}, title = {Simple unification-based type inference for {GADTs}}, booktitle = {ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming}, year = {2006}, isbn = {1-59593-309-3}, pages = {50--61}, location = {Portland, Oregon, USA}, publisher = {ACM Press}, address = {New York, NY, USA}, } @inproceedings{sulzman+:eadts, author = {Martin Sulzmann and Jeremy Wazny and Peter J. Stuckey}, title = {A Framework for Extended Algebraic Data Types.}, booktitle = {FLOPS}, year = {2006}, pages = {47-64}, ee = {http://dx.doi.org/10.1007/11737414_5}, crossref = {DBLP:conf/flops/2006}, bibsource = {DBLP, http://dblp.uni-trier.de} } @proceedings{DBLP:conf/flops/2006, editor = {Masami Hagiya and Philip Wadler}, title = {Functional and Logic Programming, 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings}, booktitle = {FLOPS}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3945}, year = {2006}, isbn = {3-540-33438-6}, bibsource = {DBLP, http://dblp.uni-trier.de} } @article{crary+:polyrecrelns, author = {Crary, Karl and Harper, Robert}, title = {Syntactic Logical Relations for Polymorphic and Recursive Types}, journal = {Electron. Notes Theor. Comput. Sci.}, volume = {172}, year = {2007}, issn = {1571-0661}, pages = {259--299}, doi = {http://dx.doi.org/10.1016/j.entcs.2007.02.010}, publisher = {Elsevier Science Publishers B. V.}, address = {Amsterdam, The Netherlands, The Netherlands}, } @INPROCEEDINGS{Was+Wei:2005, AUTHOR = {Geoffrey Washburn and Stephanie Weirich}, TITLE = {Generalizing Parametricity Using Information Flow}, BOOKTITLE = {The Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)}, YEAR = 2005, MONTH = {June}, PAGES = {62--71}, ADDRESS = {Chicago, IL}, ORGANIZATION = {{IEEE} Computer Society}, PUBLISHER= {{IEEE} Computer Society Press}, PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/lics2005.pdf}, PLCLUB = "yes", ABSTRACT = { Run-time type analysis allows programmers to easily and concisely define operations based upon type structure, such as serialization, iterators, and structural equality. However, when types can be inspected at run time, nothing is secret. A module writer cannot use type abstraction to hide implementation details from clients: clients can determine the structure of these supposedly ``abstract'' data types. Furthermore, access control mechanisms do not help isolate the implementation of abstract datatypes from their clients. Buggy or malicious authorized modules may leak type information to unauthorized clients, so module implementors cannot reliably tell which parts of a program rely on their type definitions. Currently, module implementors rely on parametric polymorphism to provide integrity and confidentiality guarantees about their abstract datatypes. However, standard parametricity does not hold for languages with run-time type analysis; this paper shows how to generalize parametricity so that it does. The key is to augment the type system with annotations about information-flow. Implementors can then easily see which parts of a program depend on the chosen implementation by tracking the flow of dynamic type information. } } @incollection{cardelli91extension, author = "Luca Cardelli and John C. Mitchell and Simone Martini and Andre Scedrov", title = "An Extension of System {F} with Subtyping", booktitle = "Proc.\ of 1st Int.\ Symp.\ on Theor.\ Aspects of Computer Software, {TACS}'91, Sendai, Japan, 24--27 Sept 1991", volume = "526", publisher = "Springer-Verlag", address = "Berlin", editor = "Takayasu Ito and Albert R. Meyer", pages = "750--770", year = "1991", url = "citeseer.ist.psu.edu/cardelli91extension.html" } @inproceedings{donnelly-xi:normalization, author = {Kevin Donnelly and Hongwei Xi}, title = "A Formalization of Strong normalization for Simply Typed Lambda-Calculus and {System F}", booktitle = {International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Seattle, WA}, year = {2006}, pages = "98--113", month = {Aug}, } @techreport{sarnat-schuermann:lr, author = "Jeffrey Sarnat and Carsten Schurmann", title = "On the representation of logical relations in {Twelf}", institution = "Yale University", year = "2006", number = "YaleU/DCS/TR-1362"} @article{harper-mitchell:joperator, author = {Robert Harper and John C. Mitchell}, title = {Parametricity and variants of {Girard's} {J} operator}, journal = {Inf. Process. Lett.}, volume = {70}, number = {1}, year = {1999}, issn = {0020-0190}, pages = {1--5}, doi = {http://dx.doi.org/10.1016/S0020-0190(99)00036-8}, publisher = {Elsevier North-Holland, Inc.}, address = {Amsterdam, The Netherlands, The Netherlands}, } @PhDThesis{KucanThesis, author = "Jacov Ku\v{c}an ", title = "Metatheorems about Convertibility in Typed Lambda Calculi: Applications to CPS Transform and Free Theorems", school = "Massachusetts Institute of Technology", month = "February", year = "1997" } @TechReport{takeuti:lambda-cube, year = {2001}, month = jun, author = {Izumi Takeuti}, title = {The Theory of Parametricity in Lambda Cube (Towards new interaction between category theory and proof theory)}, uri = {\url{http://hdl.handle.net/2433/41237}}, institution = {Kyoto University Research Information Repository} } @article{vytiniotis:rtheorems, author = {Dimitrios Vytiniotis and Stephanie Weirich}, title = {Free Theorems and Runtime Type Representations}, journal = {Electron. Notes Theor. Comput. Sci.}, volume = {173}, year = {2007}, issn = {1571-0661}, pages = {357--373}, doi = {http://dx.doi.org/10.1016/j.entcs.2007.02.043}, publisher = {Elsevier Science Publishers B. V.}, address = {Amsterdam, The Netherlands, The Netherlands}, } @inproceedings{achten+:compositional-model-views, author = {Peter Achten and Marko C. J. D. van Eekelen and Marinus J. Plasmeijer}, title = {Compositional Model-Views with Generic Graphical User Interfaces.}, booktitle = {Practical Aspects of Declarative Languages, 6th International Symposium, PADL 2004, Dallas, TX, USA, June 18-19, 2004, Proceedings}, pages = {39-55}, year = {2004}, ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3057{\&}spage=39}, bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{cheney:nameplate, author = {James Cheney}, title = {Scrap your nameplate: (functional pearl)}, booktitle = {ICFP '05: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming}, year = {2005}, isbn = {1-59593-064-7}, pages = {180--191}, location = {Tallinn, Estonia}, doi = {http://doi.acm.org/10.1145/1086365.1086389}, publisher = {ACM Press}, address = {New York, NY, USA}, } @article{pfenning:logical-frameworks, author = {Frank Pfenning}, title = {Logical frameworks}, journal = {Handbook of automated reasoning}, year = {2001}, isbn = {0-444-50812-0}, pages = {1063--1147}, publisher = {Elsevier Science Publishers B. V.}, address = {Amsterdam, The Netherlands, The Netherlands}, } @inproceedings{baars+:tdt, author = {Arthur I. Baars and S. Doaitse Swierstra}, title = {Typing dynamic typing}, booktitle = {ICFP '02: Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming}, year = {2002}, isbn = {1-58113-487-8}, pages = {157--166}, location = {Pittsburgh, PA, USA}, doi = {http://doi.acm.org/10.1145/581478.581494}, publisher = {ACM Press}, address = {New York, NY, USA}, } @inproceedings{cheney-hinze:lightweight-generics, author = {James Cheney and Ralf Hinze}, title = {A lightweight implementation of generics and dynamics}, booktitle = {Haskell '02: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell}, year = {2002}, isbn = {1-58113-605-6}, pages = {90--104}, location = {Pittsburgh, Pennsylvania}, doi = {http://doi.acm.org/10.1145/581690.581698}, publisher = {ACM Press}, address = {New York, NY, USA}, } @inproceedings{lammel:syb-xpath, author = {Ralf L\"{a}mmel}, title = {Scrap your boilerplate with {XPath}-like combinators}, booktitle = {POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages}, year = {2007}, isbn = {1-59593-575-4}, pages = {137--142}, location = {Nice, France}, doi = {http://doi.acm.org/10.1145/1190216.1190240}, publisher = {ACM Press}, address = {New York, NY, USA}, } @article{weirich:runtime, author = {Stephanie Weirich}, title = {Type-safe run-time polytypic programming}, journal = {Journal of Functional Programming}, volume = {16}, number = {6}, year = {2006}, issn = {0956-7968}, pages = {681--710}, doi = {http://dx.doi.org/10.1017/S0956796806005879}, publisher = {Cambridge University Press}, address = {New York, NY, USA}, } @inproceedings{syb3, author = {Ralf L\"{a}mmel and Simon {Peyton Jones}}, title = "{Scrap your boilerplate with class: extensible generic functions}", booktitle = "{Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP 2005)}", year = {2005}, pages = {204--215}, location = {Tallinn, Estonia}, publisher = {ACM Press}, month = sep, } @inproceedings{generic-views, author = {Stefan Holdermans and Johan Jeuring and Andres L\"{o}h and Alexey Rodriguez}, title = {Generic Views on Data Types}, booktitle = {Mathematics of Program Construction, 8th International Conference, MPC 2006, Kuressaare, Estonia, July 3-5, 2006, Proceedings}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 4014, year = 2006, isbn = {978-3-540-35631-8}, } @article{harper-pfening:canforms, author = {Robert Harper and Frank Pfenning}, title = {On equivalence and canonical forms in the {LF} type theory}, journal = {ACM Trans. Comput. Logic}, volume = {6}, number = {1}, year = {2005}, issn = {1529-3785}, pages = {61--101}, doi = {http://doi.acm.org/10.1145/1042038.1042041}, publisher = {ACM Press}, address = {New York, NY, USA}, } @inproceedings{Pau93a, Author = {Christine {Paulin-Mohring}}, Booktitle = {International Conference on Typed Lambda Calculi and Applications, TLCA '93}, Date-Modified = {2007-04-25 22:40:20 -0400}, Pages = {328--345}, Publisher = {Springer}, Series = {Lecture Notes in Computer Science}, Title = {Inductive Definitions in the System {Coq}: Rules and Properties}, Volume = {664}, Year = {1993}} @MANUAL{ghc, author = {The GHC team}, title = {The {Glasgow Haskell} compiler}, url = {http://www.haskell.org/ghc/} } @MANUAL{coq, author = {{The Coq Team}}, title = {Coq}, url = {http://coq.inria.fr} } @book{ CroleBook, author = "Roy Crole", title = "Categories for Types", publisher = "Cambridge University Press", year = "1994" } @inproceedings{dreyer:non-parametric, author = {Neis, Georg and Dreyer, Derek and Rossberg, Andreas}, title = {Non-parametric parametricity}, booktitle = {ICFP '09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming}, year = {2009}, isbn = {978-1-60558-332-7}, pages = {135--148}, location = {Edinburgh, Scotland}, publisher = {ACM}, address = {New York, NY, USA}, } # doi = {http://doi.acm.org/10.1145/1596550.1596572}, @inproceedings{voigtlander:type-constructor, author = {Voigtl\"{a}nder, Janis}, title = {Free theorems involving type constructor classes: functional pearl}, booktitle = {ICFP '09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming}, year = {2009}, isbn = {978-1-60558-332-7}, pages = {173--184}, location = {Edinburgh, Scotland}, doi = {http://doi.acm.org/10.1145/1596550.1596577}, publisher = {ACM}, address = {New York, NY, USA}, } @inproceedings{andersson+:fastandloose, abstract = {Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values, and all types are lifted, including the function spaces. A partial equivalence relation (PER) is then defined, the domain of which is the total subset of the partial language. For types not containing function spaces the PER relates equal values, and functions are related if they map related values to related values.It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the PER gives rise to a bicartesian closed category which can be used to reason about values in the domain of the relation.}, address = {New York, NY, USA}, author = {Danielsson, Nils A. and Hughes, John and Jansson, Patrik and Gibbons, Jeremy}, booktitle = {POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, citeulike-article-id = {558255}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1111037.1111056}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1111037.1111056}, comment = {* Concert Reading Group: 02/13/2006}, doi = {10.1145/1111037.1111056}, isbn = {1-59593-027-2}, keywords = {rg-2006}, location = {Charleston, South Carolina, USA}, month = {January}, number = {1}, pages = {206--217}, posted-at = {2009-08-17 19:18:44}, priority = {2}, publisher = {ACM}, title = {Fast and loose reasoning is morally correct}, url = {http://dx.doi.org/10.1145/1111037.1111056}, volume = {41}, year = {2006} } # isbn = {978-1-60558-379-2}, # doi = {http://doi.acm.org/10.1145/1480881.1480926}, @inproceedings{mongagu-remy:modules, author = {Montagu, Beno\^{\i}t and R\'{e}my, Didier}, title = {Modeling abstract types in modules with open existential types}, booktitle = {POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, year = {2009}, pages = {354--365}, location = {Savannah, GA, USA}, publisher = {ACM}, address = {New York, NY, USA}, } @phdthesis{dreyer:thesis, author = {Dreyer, Derek}, note = {Co-Chair-Harper, Robert and Co-Chair-Crary, Karl}, title = {Understanding and evolving the {ML} module system}, year = {2005}, isbn = {0-542-01550-1}, order_no = {AAI3166274}, publisher = {Carnegie Mellon University}, address = {Pittsburgh, PA, USA}, } @inproceedings{neis+:non-parametric, author = {Neis, Georg and Dreyer, Derek and Rossberg, Andreas}, title = {Non-parametric parametricity}, booktitle = {ICFP '09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming}, year = {2009}, isbn = {978-1-60558-332-7}, pages = {135--148}, location = {Edinburgh, Scotland}, publisher = {ACM}, address = {New York, NY, USA}, } # isbn = {1-59593-064-7}, # doi = {http://doi.acm.org/10.1145/1086365.1086372}, @inproceedings{dreyer:rec-param, author = {Dreyer, Derek}, title = {Recursive type generativity}, booktitle = {ICFP '05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming}, year = {2005}, pages = {41--53}, location = {Tallinn, Estonia}, publisher = {ACM}, address = {New York, NY, USA}, } # doi = {http://doi.acm.org/10.1145/888251.888274}, @inproceedings{rossberg:generativity, author = {Rossberg, Andreas}, title = {Generativity and dynamic opacity for abstract types}, booktitle = {PPDP '03: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming}, year = {2003}, isbn = {1-58113-705-2}, pages = {241--252}, location = {Uppsala, Sweden}, publisher = {ACM}, address = {New York, NY, USA}, } @article{benje+:universes, author = {Benke, Marcin and Dybjer, Peter and Jansson, Patrik}, title = {Universes for generic programs and proofs in dependent type theory}, journal = {Nordic J. of Computing}, volume = {10}, number = {4}, year = {2003}, issn = {1236-6064}, pages = {265--289}, publisher = {Publishing Association Nordic Journal of Computing}, address = {, Finland}, } # doi = {http://doi.acm.org/10.1145/1190315.1190324}, # isbn = {1-59593-393-X}, @inproceedings{sulzmann+:fc-paper, author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and {Peyton Jones}, Simon and Donnelly, Kevin}, title = {System {F} with type equality coercions}, booktitle = {TLDI '07: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation}, year = {2007}, pages = {53--66}, location = {Nice, Nice, France}, publisher = {ACM}, address = {New York, NY, USA}, } @article{haskell98, author = {Simon {Peyton Jones} and others}, title = {The {Haskell} 98 Language and Libraries: The Revised Report}, journal = {Journal of Functional Programming}, volume = 13, number = 1, pages = {0--255}, month = {Jan}, year = 2003, note = {\url{http://www.haskell.org/definition/}}, } # doi = {http://doi.acm.org/10.1145/1047659.1040306}, @article{chak+:types, author = {Chakravarty, Manuel M. T. and Keller, Gabriele and {Peyton Jones}, Simon and Marlow, Simon}, title = {Associated types with class}, journal = {SIGPLAN Not.}, volume = {40}, number = {1}, year = {2005}, issn = {0362-1340}, pages = {1--13}, publisher = {ACM}, address = {New York, NY, USA}, } # doi = {http://doi.acm.org/10.1145/1086365.1086397}, # isbn = {1-59593-064-7}, @inproceedings{chak+:synonyms, author = {Chakravarty, Manuel M. T. and Keller, Gabriele and {Peyton Jones}, Simon}, title = {Associated type synonyms}, booktitle = {ICFP '05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming}, year = {2005}, pages = {241--253}, location = {Tallinn, Estonia}, publisher = {ACM}, address = {New York, NY, USA}, } @inproceedings{Kiselyov09funwith, author = {Oleg Kiselyov and Simon {Peyton Jones} and {Chung-chieh} Shan}, title = {Fun with type functions}, booktitle = "Reflections on the work of CAR Hoare", editor = "Cliff Jones and Bill Roscoe", publisher = "Springer", year = {2010} } @inproceedings{russo:existentials, author = {Russo, Claudio V.}, title = {Non-dependent Types for {Standard ML} Modules}, booktitle = {PPDP '99: Proceedings of the International Conference PPDP'99 on Principles and Practice of Declarative Programming}, year = {1999}, isbn = {3-540-66540-4}, pages = {80--97}, publisher = {Springer-Verlag}, address = {London, UK}, } @book{sml-book, author = {Milner, Robin and Tofte, Mads and Macqueen, David}, title = {The Definition of Standard ML}, year = {1997}, isbn = {0262631814}, publisher = {MIT Press}, address = {Cambridge, MA, USA}, } @article{dybjer:ind-rec, author = {Peter Dybjer}, title = {A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory}, journal = { Journal of Symbolic Logic}, year = 2000, volume = 65, number = 2, pages = {525--549} } # isbn = {978-1-59593-919-7}, # doi = {http://doi.acm.org/10.1145/1411204.1411215}, @inproceedings{shrijvers:open-tyfuns, author = {Schrijvers, Tom and {Peyton Jones}, Simon and Chakravarty, Manuel and Sulzmann, Martin}, title = {Type checking with open type functions}, booktitle = {ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming}, year = {2008}, pages = {51--62}, location = {Victoria, BC, Canada}, publisher = {ACM}, address = {New York, NY, USA}, } # doi = {http://dx.doi.org/10.1007/978-3-642-03359-9_6}, # isbn = {978-3-642-03358-2}, @inproceedings{agda, author = {Bove, Ana and Dybjer, Peter and Norell, Ulf}, title = {A Brief Overview of {Agda} --- A Functional Language with Dependent Types}, booktitle = {TPHOLs '09: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics}, year = {2009}, pages = {73--78}, location = {Munich, Germany}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @phdthesis{norell:thesis, author = {Ulf Norell}, title = {Towards a practical programming language based on dependent type theory}, school = {Department of Computer Science and Engineering, Chalmers University of Technology}, year = 2007, month = {September}, address = {SE-412 96 G\"{o}teborg, Sweden} } @TechReport{lh05dmlproofs-tr, author = {Daniel R. Licata and Robert Harper}, title = {A Formulation of Dependent {ML} with Explicit Equality Proofs}, institution = {Carnegie Mellon University Department of Computer Science}, year = {2005}, number = {CMU-CS-05-178}, } # doi = {http://doi.acm.org/10.1145/1053468.1053469}, # issn = {0164-0925}, @article{shao+:certbin, author = {Shao, Zhong and Trifonov, Valery and Saha, Bratin and Papaspyrou, Nikolaos}, title = {A type system for certified binaries}, journal = {ACM Trans. Program. Lang. Syst.}, volume = {27}, number = {1}, year = {2005}, pages = {1--45}, publisher = {ACM}, address = {New York, NY, USA}, } @BOOK{ATTAPL, EDITOR = {Benjamin C. Pierce}, TITLE = {Advanced Topics in Types and Programming Languages}, PUBLISHER = {MIT Press}, YEAR = 2005, PLCLUB = {Yes}, BCP = {Yes}, KEYS = {books}, HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/attapl} } @inproceedings{weirich+:fc2, author = {Weirich, Stephanie and Vytiniotis, Dimitrios and Peyton Jones, Simon and Zdancewic, Steve}, title = {Generative type abstraction and type-level computation}, booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on {Principles} of {Programming} {Languages}}, series = {POPL '11}, year = {2011}, isbn = {978-1-4503-0490-0}, location = {Austin, Texas, USA}, pages = {227--240}, numpages = {14}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {haskell, newtype deriving, type functions}, } @inproceedings{HarperM95, author = {Robert Harper and Greg Morrisett}, title = {Compiling polymorphism using intensional type analysis}, booktitle = {POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, year = {1995}, isbn = {0-89791-692-1}, pages = {130--141}, location = {San Francisco, California, United States}, publisher = {ACM}, address = {New York, NY, USA}, ps = {http://www.eecs.harvard.edu/~greg/papers/ip-popl.ps} } @inproceedings{Altenkirch:ott, author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter}, title = {Observational equality, now!}, booktitle = {Proceedings of the 2007 workshop on Programming languages meets program verification}, series = {PLPV '07}, year = {2007}, isbn = {978-1-59593-677-6}, location = {Freiburg, Germany}, pages = {57--68}, numpages = {12}, url = {http://doi.acm.org/10.1145/1292597.1292608}, doi = {http://doi.acm.org/10.1145/1292597.1292608}, acmid = {1292608}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {equality, type theory}, } @article{ott1, author = {Thorsten Altenkirch and Conor McBride}, title = {Towards Observational Type Theory}, masid = {4008452} } @inproceedings{Miquel:icc, author = {Miquel, Alexandre}, title = {The implicit calculus of constructions: extending pure type systems with an intersection type binder and subtyping}, booktitle = {Proceedings of the 5th international conference on Typed lambda calculi and applications}, series = {TLCA'01}, year = {2001}, isbn = {3-540-41960-8}, location = {Krak\&\#243;w, Poland}, pages = {344--359}, numpages = {16}, url = {http://portal.acm.org/citation.cfm?id=1754621.1754650}, acmid = {1754650}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @inproceedings{barras:icc, author = {Bruno Barras and Bruno Bernardo}, title = {The Implicit Calculus of Constructions as a Programming Language with Dependent Types}, booktitle = {Foundations of Software Science and Computation Structure}, year = {2008}, pages = {365--379}, doi = {10.1007/978-3-540-78499-9_26}, masid = {4259647} } @InProceedings{swamy+:fstar, author = {Nikhil Swamy and Juan Chen and Cedric Fournet and Pierre-Yves Strub and Karthikeyan Bharagavan and Jean Yang}, title = {Secure Distributed Programming with Value-dependent Types}, booktitle = {Proceedings of the Sixteenth {ACM SIGPLAN} International Conference on Functional Programming (ICFP '11)}, year = 2011, month = {September}, note = {To appear.} } @inproceedings{tldi12, author = {Yorgey, Brent A. and Weirich, Stephanie and Cretin, Julien and Peyton Jones, Simon and Vytiniotis, Dimitrios and Magalh\~aes, Jos\'e Pedro}, title = {Giving {Haskell} a Promotion}, booktitle = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation}, series = {TLDI '12}, year = {2012}, location = {Philadelphia, PA, USA}, pages = {53--66}, doi = {10.1145/2103786.2103795}, publisher = {ACM}, address = {New York, NY, USA}, } @inproceedings{flanagan-hybrid, author = {Flanagan, Cormac}, title = {Hybrid type checking}, booktitle = {Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, series = {POPL '06}, year = {2006}, isbn = {1-59593-027-2}, location = {Charleston, South Carolina, USA}, pages = {245--256}, numpages = {12}, url = {http://doi.acm.org/10.1145/1111037.1111059}, doi = {http://doi.acm.org/10.1145/1111037.1111059}, acmid = {1111059}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {contracts, dynamic checking, static checking, type systems}, } @inproceedings{wadler-blame-calculus, author = {Wadler, Philip and Findler, Robert Bruce}, title = {Well-Typed Programs Can't Be Blamed}, booktitle = {Proceedings of the 18th European Symposium on Programming Languages and Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009}, series = {ESOP '09}, year = {2009}, isbn = {978-3-642-00589-3}, location = {York, UK}, pages = {1--16}, numpages = {16}, url = {http://dx.doi.org/10.1007/978-3-642-00590-9_1}, doi = {http://dx.doi.org/10.1007/978-3-642-00590-9_1}, acmid = {1532976}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, } @inproceedings{blame-for-all, author = {Ahmed, Amal and Findler, Robert Bruce and Matthews, Jacob and Wadler, Philip}, title = {Blame for all}, booktitle = {Proceedings for the 1st workshop on Script to Program Evolution}, series = {STOP '09}, year = {2009}, isbn = {978-1-60558-543-7}, location = {Genova, Italy}, pages = {1--13}, numpages = {13}, url = {http://doi.acm.org/10.1145/1570506.1570507}, doi = {http://doi.acm.org/10.1145/1570506.1570507}, acmid = {1570507}, publisher = {ACM}, address = {New York, NY, USA}, } @InProceedings{siek08:_gradual_inference, author = {Jeremy G. Siek and Manish Vachharajani}, title = {Gradual Typing with Unification-based Inference}, booktitle = {Dynamic Languages Symposium}, abstract = {Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence or absence of type annotations. This paper studies the combination of gradual typing and unification-based type inference with the goal of developing a system that helps programmers increase the amount of static checking in their program. The key question in combining gradual typing and type inference is how should the dynamic type of a gradual system interact with the type variables of a type inference system. This paper explores the design space and shows why three straightforward approaches fail to meet our design goals. This paper presents a new type system based on the idea that a solution for a type variable should be as informative as any type that constrains the variable. The paper also develops an efficient inference algorithm and proves it sound and complete with respect to the type system. }, year = 2008, month = {July} } @InProceedings{siek06:_gradual, author = {Jeremy G. Siek and Walid Taha}, title = {Gradual typing for functional languages}, booktitle = {Scheme and Functional Programming Workshop}, year = 2006, month = {September} } @article{type-error-slicing, author = {Haack, Christian and Wells, J. B.}, title = {Type error slicing in implicitly typed higher-order languages}, journal = {Sci. Comput. Program.}, volume = {50}, issue = {1-3}, month = {March}, year = {2004}, issn = {0167-6423}, pages = {189--224}, numpages = {36}, url = {http://dl.acm.org/citation.cfm?id=989777.989786}, doi = {10.1016/j.scico.2004.01.004}, acmid = {989786}, publisher = {Elsevier North-Holland, Inc.}, address = {Amsterdam, The Netherlands, The Netherlands}, keywords = {intersection types, type error location, type inference}, } @inproceedings{Tobin-Hochstadt:migration, author = {Tobin-Hochstadt, Sam and Felleisen, Matthias}, title = {Interlanguage migration: from scripts to programs}, booktitle = {Companion to the 21st ACM SIGPLAN symposium on Object-oriented programming systems, languages, and applications}, series = {OOPSLA '06}, year = {2006}, isbn = {1-59593-491-X}, location = {Portland, Oregon, USA}, pages = {964--974}, numpages = {11}, url = {http://doi.acm.org/10.1145/1176617.1176755}, doi = {http://doi.acm.org/10.1145/1176617.1176755}, acmid = {1176755}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {{\$\lambda\$}-calculus, contract, interlanguage migration, module systems}, } @book{MacLaneS:catwm, author = {Mac Lane, Saunders}, title = {Categories for the Working Mathematician}, publisher = {Springer-Verlag}, series = {Graduate Texts in Mathematics}, number = 5, year = 1971, isbn = 0387900357} @inproceedings{Licata:2012:CTT:2103656.2103697, author = {Licata, Daniel R. and Harper, Robert}, title = {Canonicity for 2-dimensional type theory}, booktitle = {Proceedings of the 39th annual ACM SIGPLAN-SIGACT {Symposium} on {Principles} of {Programming} {Languages}}, series = {POPL '12}, year = {2012}, isbn = {978-1-4503-1083-3}, location = {Philadelphia, PA, USA}, pages = {337--348}, numpages = {12}, url = {http://doi.acm.org/10.1145/2103656.2103697}, doi = {10.1145/2103656.2103697}, acmid = {2103697}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {category theory, dependent types, homotopy type theory, type theory}, } @book{Baader:1998:TR:280474, author = {Baader, Franz and Nipkow, Tobias}, title = {Term rewriting and all that}, year = {1998}, isbn = {0-521-45520-0}, publisher = {Cambridge University Press}, address = {New York, NY, USA}, } @inproceedings{Dershowitz:1983:AR:1623516.1623594, author = {Dershowitz, Nachum and Hsiang, Jien and Josephson, N. Alan and Plaisted, David A.}, title = {Associative-commutative rewriting}, booktitle = {Proceedings of the Eighth international joint conference on Artificial intelligence - Volume 2}, series = {IJCAI'83}, year = {1983}, location = {Karlsruhe, West Germany}, pages = {940--944}, numpages = {5}, url = {http://dl.acm.org/citation.cfm?id=1623516.1623594}, acmid = {1623594}, publisher = {Morgan Kaufmann Publishers Inc.}, address = {San Francisco, CA, USA}, } @article{Bachmair:1985:TOA:6947.6948, author = {Bachmair, Leo and Plaisted, David A.}, title = {Termination orderings for associative-commutative rewriting systems}, journal = {J. Symb. Comput.}, issue_date = {Dec. 1985}, volume = {1}, number = {4}, month = dec, year = {1985}, issn = {0747-7171}, pages = {329--349}, numpages = {21}, url = {http://dx.doi.org/10.1016/S0747-7171(85)80019-5}, doi = {10.1016/S0747-7171(85)80019-5}, acmid = {6948}, publisher = {Academic Press, Inc.}, address = {Duluth, MN, USA}, }