max.bib

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                       String Definitions                         %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Publishing houses
% %%%%%%%%%%%%%%%%%
@STRING{ap =        "Academic Press" }
@STRING{springer =  {Springer-Verlag} }
@STRING{lncs =      "Lecture Notes in Computer Science" }
@STRING{lnm =       "Lecture Notes in Mathematics" }
@STRING{gtm =       "Graduate Texts in Mathematics" }
@STRING{lfcs =      "Laboratory for Foundations of Computer Science,
                    University of Edinburgh" }
@STRING{mp =        "MIT Press" }
@STRING{mitpress =  mp }
%
% Journals and magazines
% %%%%%%%%%%%%%%%%%%%%%%
@STRING{toplas =    "ACM Transactions on Programming Languages and Systems" }
@STRING{jlp =       {Journal of Logic Programming} }
@STRING{cacm =      "Communications of the {ACM}" }
@STRING{jacm =      "Journal of the {ACM}" }
@STRING{tcs =       "Theoretical Computer Science" }
@STRING{jsl =       "Journal of Symbolic Logic" }
@STRING{siamjc =    "SIAM Journal on Computing" }
@STRING{mscs =      "Mathematical Structures in Computer Science" }
@STRING{proc =      "Proceedings of the" }
@STRING{ic =        "Information and Computation" }
@STRING{iandcomp =  {Information and Computation} }
@string{ifip =      "International Federation for Information Processing World Computer Congress (IFIP)"}
@STRING{jfp =       "Journal of Functional Programming" }
@STRING{lmcs =      "Logical Methods in Computer Science" }
@string{hosc =      "Higher-Order and Symbolic Computation"}
@STRING{cup =       "Cambridge University Press" }
@STRING{mcgh =      "McGraw-Hill" }
@STRING{nh =        "North Holland" }
@STRING{sv =        "Springer-Verlag" }
@STRING{aw =        "Addison-Wesley" }
@STRING{ph =        "Prentice Hall" }
@STRING{signot =    "SIGPLAN Notices"}
@STRING{taoop =     "Carl A. Gunter and John C. Mitchell, editors, {\em
                    Theoretical Aspects of Object-Oriented Programming:
                    Types, Semantics, and Language Design}, MIT Press, 1994" }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                             Conferences                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@STRING{popl =      "{ACM} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL})" }
@STRING{popl73 =    popl # ", Boston, Massachusetts" }
@STRING{popl75 =    popl # ", Palo Alto, California" }
@STRING{popl76 =    popl # ", {A}tlanta, {G}eorgia" }
@STRING{popl77 =    popl # ", Los Angeles, California" }
@STRING{popl78 =    popl # ", Tucson, Arizona" }
@STRING{popl79 =    popl # ", San Antonio, Texas" }
@STRING{popl80 =    popl # ", Las Vegas, Nevada" }
@STRING{popl81 =    popl # ", Williamsburg, Virginia" }
@STRING{popl82 =    popl # ", Albuquerque, New Mexico" }
@STRING{popl83 =    popl # ", Austin, Texas" }
@STRING{popl84 =    popl # ", Salt Lake City, Utah" }
@STRING{popl85 =    popl # ", New Orleans, Louisiana" }
@STRING{popl86 =    popl # ", St.\ Petersburg Beach, Florida" }
@STRING{popl87 =    popl # ", Munich, Germany" }
@STRING{popl88 =    popl # ", San Diego, California" }
@STRING{popl89 =    popl # ", Austin, Texas" }
@STRING{popl90 =    popl # ", {S}an {F}rancisco, {C}alifornia" }
@STRING{popl91 =    popl # ", Orlando, Florida" }
@STRING{popl92 =    popl # ", Albuquerque, New Mexico" }
@STRING{popl93 =    popl # ", Charleston, South Carolina" }
@STRING{popl94 =    popl # ", {P}ortland, {O}regon" }
@STRING{popl95 =    popl # ", San Francisco, California" }
@STRING{popl96 =    popl # ", St.~Petersburg Beach, Florida" }
@STRING{popl97 =    popl # ", Paris, France" }
@STRING{popl98 =    popl # ", San Diego, California" }
@STRING{popl99 =    popl # ", San Antonio, Texas" }
@STRING{popl00 =    popl # ", Boston, Massachusetts" }
@STRING{popl01 =    popl # ", London, England" }
@STRING{popl02 =    popl # ", Portland, Oregon" }
@STRING{popl03 =    popl # ", New Orleans, Louisiana" }
@STRING{popl04 =    popl # ", Venice, Italy" }
@STRING{popl05 =    popl # ", Long Beach, California" }
@STRING{popl06 =    popl # ", Charleston, South Carolina" }
@STRING{popl07 =    popl # ", Nice, France" }
@STRING{popl08 =    popl # ", San Francisco, California" }
@STRING{popl09 =    popl # ", Savannah, Georgia" }
@STRING{popl10 =    popl # ", Madrid, Spain" }
@STRING{popl11 =    popl # ", Austin, Texas" }
@STRING{popl12 =    popl # ", Philadelphia, Pennsylvania" }
@STRING{popl13 =    popl # ", Rome, Italy" }
@STRING{popl14 =    popl # ", San Diego, California" }
@STRING{popl15 =    popl # ", Mumbai, India" }
@STRING{popl16 =    popl # ", St. Petersburg, Florida" }
% ----
@STRING{icfp =      "{I}nternational {C}onference on {F}unctional {P}rogramming
                    ({ICFP})" }
@STRING{icfp96 =    icfp # ", Philadelphia, Pennsylvania" }
@STRING{icfp97 =    icfp # ", Amsterdam, The Netherlands" }
@STRING{icfp98 =    icfp # ", Baltimore, Maryland, USA" }
@STRING{icfp99 =    icfp # ", Paris, France" }
@STRING{icfp00 =    icfp # ", Montreal, Canada" }
@STRING{icfp01 =    icfp # ", Firenze, Italy" }
@STRING{icfp02 =    icfp # ", Pittsburgh, Pennsylvania" }
@STRING{icfp03 =    icfp # ", Uppsala, Sweden" }
@STRING{icfp04 =    icfp # ", Snowbird, Utah" }
@STRING{icfp05 =    icfp # ", Tallinn, Estonia" }
@STRING{icfp06 =    icfp # ", Portand, Oregon" }
@STRING{icfp07 =    icfp # ", Freiburg, Germany" }
@STRING{icfp08 =    icfp # ", Victoria, British Columbia, Canada" }
@STRING{icfp09 =    icfp # ", Edinburgh, Scotland" }
@STRING{icfp10 =    icfp # ", Baltimore, Maryland" }
@STRING{icfp11 =    icfp # ", Tokyo, Japan" }
@STRING{icfp12 =    icfp # ", Copenhagen, Denmark" }
@STRING{icfp13 =    icfp # ", Boston, Massachusetts" }
@STRING{icfp14 =    icfp # ", Gothenburg, Sweden" }
@STRING{icfp15 =    icfp # ", Vancouver, British Columbia, Canada" }
@STRING{icfp16 =    icfp # ", Nara, Japan" }
@STRING{icfp17 =    icfp # ", Oxford, United Kingdom" }
@STRING{icfp18 =    icfp # ", St. Louis, Missouri" }

% ----
@STRING{oopsla =    "{ACM} {S}ymposium on {O}bject {O}riented {P}rogramming:
                    {S}ystems, {L}anguages, and {A}pplications ({OOPSLA})" }
@STRING{oopsla86 =  oopsla # ", Portland, Oregon" }
@STRING{oopsla89 =  oopsla }
@STRING{oopsla98 =  oopsla # ", Vancouver, British Columbia" }
@STRING{oopsla08 =  oopsla # ", Nashville, Tennessee" }
% ----
@STRING{lics =      "IEEE Symposium on Logic in Computer Science (LICS)" }
@STRING{lics91 =    lics # ", Amsterdam, The Netherlands" }
@STRING{lics92 =    lics # ", Santa Cruz, California" }
@STRING{lics93 =    lics # ", Montreal, Canada" }
@STRING{lics94 =    lics # ", Paris, France" }
@STRING{lics95 =    lics # ", San Diego, California" }
@STRING{lics96 =    lics # ", New Brunswick, New Jersey" }
@STRING{lics97 =    lics # ", Warsaw, Poland" }}
@STRING{lics98 =    lics # ", Indianapolis, Indiana" }
@STRING{lics99 =    lics # ", Trento, Italy" }
@STRING{lics00 =    lics # ", Santa Barbara, California" }
@STRING{lics01 =    lics # ", Boston, Massachusetts" }
@STRING{lics02 =    lics # ", Copenhagen, Denmark" }
@STRING{lics03 =    lics # ", Ottawa, Canada" }
@STRING{lics04 =    lics # ", Turku, Finland" }
@STRING{lics05 =    lics # ", Chicago, Illinois" }
@STRING{lics06 =    lics # ", Seattle, Washington" }
@STRING{lics07 =    lics # ", Wroclaw, Poland" }
@STRING{lics08 =    lics # ", Pittsburgh, Pennsylvania" }
@STRING{lics09 =    lics # ", Los Angeles, California" }
@STRING{lics10 =    lics # ", Edinburgh, Scotland" }
@STRING{lics11 =    lics # ", Toronto, Canada" }
@STRING{lics12 =    lics # ", Dubrovnik, Croatia" }
@STRING{lics13 =    lics # ", New Orleans, Louisiana" }
@STRING{lics14 =    lics # ", Vienna, Austria" }
% ----
@STRING{pldi =      "{ACM SIGPLAN Conference on Programming Language Design
                    and Implementation (PLDI)}" }
@STRING{pldi88 =    pldi # ", {A}tlanta, {G}eorgia" }
@STRING{pldi89 =    pldi # ", Portland, Oregon" }
@STRING{pldi90 =    pldi # ", White Plains, New York" }
@STRING{pldi91 =    pldi # ", Toronto, Ontario" }
@STRING{pldi92 =    pldi # ", San Francisco, California" }
@STRING{pldi93 =    pldi # ", Albuquerque, New Mexico" }
@STRING{pldi94 =    pldi # ", Orlando, Florida" }
@STRING{pldi95 =    pldi # ", La Jolla, California" }
@STRING{pldi96 =    pldi # ", Philadephia, Pennsylvania" }
@STRING{pldi97 =    pldi # ", Las Vegas, Nevada" }
@STRING{pldi98 =    pldi # ", {M}ontreal, {C}anada" }
@STRING{pldi99 =    pldi # ", {A}tlanta, {G}eorgia" }
@STRING{pldi00 =    pldi # ", Vancouver, British Columbia, Canada" }
@STRING{pldi01 =    pldi # ", Snowbird, Utah" }
@STRING{pldi02 =    pldi # ", Berlin, Germany" }
@STRING{pldi03 =    pldi # ", San Diego, California" }
@STRING{pldi04 =    pldi # ", Washington, DC" }
@STRING{pldi05 =    pldi # ", Chicago, Illinois" }
@STRING{pldi06 =    pldi # ", Ottawa, Canada" }
@STRING{pldi07 =    pldi # ", San Diego, California" }
@STRING{pldi08 =    pldi # ", Tucson, Arizona" }
@STRING{pldi09 =    pldi # ", Dublin, Ireland" }
@STRING{pldi10 =    pldi # ", Toronto, Canada" }
@STRING{pldi11 =    pldi # ", San Jose, California" }
@STRING{pldi12 =    pldi # ", Beijing, China" }
@STRING{pldi13 =    pldi # ", Seattle, Washington" }
@STRING{pldi14 =    pldi # ", Edinburgh, Scotland" }
% ----
@STRING{lfp =       "ACM Symposium on Lisp and Functional Programming (LFP)" }
@STRING{lfp84 =     lfp # ", Austin, Texas" }
@STRING{lfp88 =     lfp # ", Snowbird, Utah" }
@STRING{lfp90 =     lfp }
@STRING{lfp92 =     lfp }
% ----
@STRING{fpca =      "ACM Symposium on Functional Programming Languages and
                    Computer Architecture (FPCA)" }
@STRING{fpca89 =    fpca }
@STRING{fpca93 =    fpca }
% ----
@STRING{sosp=" {ACM} {S}ymposium on {O}perating {S}ystems {P}rinciples ({SOSP})"}
% ----
@STRING{fool =      "Workshop on Foundations of Object-Oriented Languages
                    (FOOL), informal proceedings" }
@STRING{tlca =      "Typed Lambda Calculi and Applications (TLCA)" }
@STRING{tlca93 =    tlca # ", Utrecht, The Netherlands" }
@STRING{tlca95 =    tlca # ", Edinburgh, UK" }
@STRING{tlca97 =    tlca # ", Nancy, France" }
@STRING{tlca99 =    tlca # ", L'Aquila, Italy" }
@STRING{tlca01 =    tlca # ", Krakow, Poland" }
@STRING{tlca03 =    tlca # ", Valencia, Spain" }
@STRING{tlca05 =    tlca # ", Nara, Japan" }
@STRING{tlca07 =    tlca # ", Paris, France" }
@STRING{tlca09 =    tlca # ", Brasilia, Brazil" }
@STRING{tlca11 =    tlca # ", Novi Sad, Serbia" }
@STRING{tlca13 =    tlca # ", Eindhoven, The Netherlands" }

@string{cav =       "Conference on Computer Aided Verification (CAV)"}
@string{ccs =       "ACM Conference on Computer and Communication Security (CCS)"}
@string{oakland =   "{IEEE} Symposium on Security and Privacy"}
@string{dls =       "Dynamic Languages Symposium (DLS)"}
@STRING{esop =      "European Symposium on Programming (ESOP)" }
@STRING{esop92 =    esop # ", Rennes, France" }
@STRING{ecoop =     "{E}uropean {C}onference on {O}bject-{O}riented
                    {P}rogramming ({ECOOP})" }
@STRING{ecoop97 =   ecoop }
@STRING{ecoop02 =   ecoop # ", Malaga, Spain" }
@STRING{flops =     "International Symposium on Functional and Logic Programming (FLOPS)" }
@STRING{flops02 =   flops # ", Aizu, Japan" }
@string{icalp =     "International Colloquium on Automata, Languages and Programming (ICALP)"}
@string{plpv =      "Programming Languages meets Program Verification (PLPV)"}
@STRING{post =      "Principles of Security and Trust (POST)" }
@string{ppdp =      "ACM Conference on Principles and Practice of Declarative Programming (PPDP)"}
@string{scheme =    "Scheme and Functional Programming Workshop (Scheme)"}
@string{stop =      "Workshop on Script-to-Program Evolution (STOP)"}
@string{tldi =      "ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI)"}
@STRING{tacs =      "Theoretical Aspects of Computer Software (TACS)" }
@STRING{tacs01 =    tacs # ", Sendai, Japan" }
@string{tfp =       "Trends in Functional Programming (TFP)"}
@STRING{webdb =     {International Workshop on the Web and Databases
                    (WebDB)} }
@STRING{langsec = "Language-theoretic Security IEEE Security and Privacy Workshop (LangSec)"}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@incollection{scott71,
  title={Continuous lattices},
  author={Scott, Dana},
  booktitle={Toposes, algebraic geometry and logic},
  pages={97--136},
  year={1972},
}

@article{scott76,
  title={Data types as lattices},
  author={Scott, Dana},
  journal={Siam Journal on computing},
  volume={5},
  number={3},
  pages={522--587},
  year={1976},
  publisher={SIAM}
}

@inproceedings{wadler-findler09,
 author = "Philip Wadler and Robert Bruce Findler",
 title = "Well-typed programs can't be blamed",
 booktitle = esop,
 year = 2009,
 month = mar,
 pages = "1--16",
 location = "York, UK"
}

@inproceedings{tobin-hochstadt06,
 author = "Sam Tobin-Hochstadt and Matthias Felleisen",
 title = "Interlanguage Migration: From Scripts to Programs",
 booktitle = dls,
 month = oct,
 pages = "964--974",
 year = 2006,
}

@inproceedings{tobin-hochstadt08,
 author = {Sam Tobin-Hochstadt and Matthias Felleisen},
 title = {The Design and Implementation of Typed Scheme},
 booktitle = popl08,
 year = {2008}}

@inproceedings{siek-taha06,
 author = "Jeremy G. Siek and Walid Taha",
 title = "Gradual Typing for Functional Languages",
 booktitle = scheme,
 month = sep,
 pages = "81--92",
 year = 2006
}

@inproceedings{scott80,
  author="Dana S. Scott",
  booktitle="To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism",
  editor="J.P. Seldin and J.R. Hindley",
  title="Relating Theories of the Lambda-Calculus",
  year=1980,
  pages="403--450"}

@inproceedings{findler-felleisen02,
author = {Robert Bruce Findler and Matthias Felleisen},
title = {Contracts for higher-order functions},
booktitle = icfp,
year = {2002},
month = sep,
pages = {48--59}
}

@inproceedings{findler-blume06,
 author = "Robby Findler and Matthias Blume",
 title = "Contracts as Pairs of Projections",
 booktitle = flops,
 month = apr,
 year = 2006,
}
@inproceedings{siek-wadler10,
  author    = {Jeremy G. Siek and Philip Wadler},
  title     = {Threesomes, with and without blame},
  booktitle = popl,
  pages     = {365--376},
  year      = {2010},
}

@inproceedings{longley03,
  title={Universal types and what they are good for},
  author={Longley, John R},
  booktitle={Domain theory, logic and computation},
  pages={25--63},
  year={2003},
}
@inproceedings{dimoulas12,
title = "Complete Monitors for Behavioral Contracts",
author = "Christos Dimoulas and Sam Tobin-Hochstadt and Matthias Felleisen",
booktitle = esop,
year = 2012,
month = mar}
@inproceedings{mz2015functors,
 author = {Melli\`{e}s, Paul-Andr{\'e} and Zeilberger, Noam},
 title = {Functors Are Type Refinement Systems},
 booktitle = {Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '15},
 year = {2015},
 isbn = {978-1-4503-3300-9},
 location = {Mumbai, India},
 pages = {3--16},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2676726.2676970},
 doi = {10.1145/2676726.2676970},
 acmid = {2676970},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {category theory, refinement types, type theory},
} 
@article{mz2015isbellpreprint,
  author    = {Paul{-}Andr{\'{e}} Melli{\`{e}}s and
               Noam Zeilberger},
  title     = {Isbell Duality for Refinement Types},
  journal   = {CoRR},
  volume    = {abs/1501.05115},
  year      = {2015},
  url       = {http://arxiv.org/abs/1501.05115},
  timestamp = {Mon, 02 Feb 2015 14:12:25 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/MelliesZ15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{mz2016bifibrational,
  author    = {Paul{-}Andr{\'{e}} Melli{\`{e}}s and
               Noam Zeilberger},
  title     = {A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine},
  booktitle = {Proceedings of the 31st Annual {ACM/IEEE} Symposium on Logic in Computer
               Science, {LICS} '16, New York, NY, USA, July 5-8, 2016},
  pages     = {555--564},
  year      = {2016},
  crossref  = {DBLP:conf/lics/2016},
  url       = {http://doi.acm.org/10.1145/2933575.2934525},
  doi       = {10.1145/2933575.2934525},
  timestamp = {Thu, 27 Oct 2016 11:27:54 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/lics/MelliesZ16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@article{shulman2008framed,
  title={Framed bicategories and monoidal fibrations},
  author={Shulman, Michael},
  journal={Theory and Applications of Categories},
  volume={20},
  number={18},
  pages={650--738},
  year={2008}
}

@article{courser2016bicategory,
  title={A bicategory of decorated cospans},
  author={Courser, Kenny},
  journal={arXiv preprint arXiv:1605.08100},
  year={2016}
}

@article{garner2006,
author = {Garner, Richard},
journal = {Cahiers de Topologie et Géométrie Différentielle Catégoriques},
number = 4,
pages = {261-317},
title = {Double clubs},
volume = 47,
year = 2006,
}

@misc{shulman2009lax,
  title = {The Problem with Lax Functors},
  author = {Shulman, Mike},
  howpublished = {\url{https://golem.ph.utexas.edu/category/2009/12/the_problem_with_lax_functors.html}},
  note = {Accessed: 2016-11-22},
}

@misc{harley,
  title = {The Combination of Dynamic and Static Typing from a Categorical Perspective},
  author = {Harley Eades III and Michael Townsend},
  howpublished = {\url{http://metatheorem.org/includes/pubs/Grady-Draft.pdf}},
  year={2017},
  note = {Accessed: 2017-7-7},
}


@article{hayashi85,
  author    = {Susumu Hayashi},
  title     = {Adjunction of Semifunctors: Categorical Structures in Nonextensional
               Lambda Calculus},
  journal   = {Theor. Comput. Sci.},
  volume    = {41},
  pages     = {95--104},
  year      = {1985},
}

@article{felleisen90,
  title={On the expressive power of programming languages},
  author={Felleisen, Matthias},
  journal={ESOP'90},
  year={1990},
}
@article{benton05:embedded,
  title={Embedded Interpreters},
  author={Nick Benton},
  journal=jfp,
  volume={15},
  number={04},
  pages={503--542},
  year={2005},
  publisher={Cambridge Univ Press}
}
@article{henglein94:dynamic-typing,
 author="Fritz Henglein",
 title="Dynamic Typing: Syntax and Proof Theory",
 journal=scp,
 volume="22",
 number="3",
 pages="197--230",
 year="1994"
}
@article{favonia17,
 title={Correctness of compiling polymorphism to dynamic typing},
 volume={27},
 journal={Journal of Functional Programming},
 author={Keun-Bang Hou (Favonia) and Nick Benton and Robert Harper},
 year={2017}
}
@inproceedings{AGT,
 author = {Garcia, Ronald and Clark, Alison M. and Tanter, \'{E}ric},
 title = {Abstracting Gradual Typing},
 booktitle = popl,
 year={2016}
}
@article{pitts96,
title = "Relational Properties of Domains",
journal = "Information and Computation",
volume = "127",
number = "2",
pages = "66 - 90",
year = "1996",
author = "Andrew M. Pitts",
}

@article{smythplotkin,
  title={The category-theoretic solution of recursive domain equations},
  author={Smyth, Michael B and Plotkin, Gordon D},
  journal={SIAM Journal on Computing},
  volume={11},
  number={4},
  year={1982},
}

@inproceedings{refined,
 author={Jeremy Siek and Micahel Vitousek and Matteo Cimini and John Tang Boyland},
 title={Refined Criteria for Gradual Typing},
 booktitle = "1st Summit on Advances in Programming Languages",
 series={SNAPL 2015},
 year={2015},
}
@inproceedings{gradualizer16,
 author = {Cimini, Matteo and Siek, Jeremy G.},
 title = {The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems},
 booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 series = {POPL '16},
 year={2016}                 
}
@inproceedings{gradualizer17,
 author = {Cimini, Matteo and Siek, Jeremy G.},
 title = {Automatically Generating the Dynamic Semantics of Gradually Typed Languages},
 booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
 series = {POPL 2017},
 year = {2017},
 pages = {789--803},
}

@inproceedings{gradeffects2014,
 author = {Ba\~{n}ados Schwerter, Felipe and Garcia, Ronald and Tanter, \'{E}ric},
 title = {A Theory of Gradual Effect Systems},
 booktitle = {Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '14},
 location = {Gothenburg, Sweden},
 pages = {283--295},
 year={2014}                  
} 

@inproceedings{disney2011gradual,
  title={Gradual information flow typing},
  author={Disney, Tim and Flanagan, Cormac},
  booktitle={International Workshop on Scripts to Programs 2011},
  year={2011}
}

@inproceedings{ahmed17,
author = {Amal Ahmed and Dustin Jamner and Jeremy G. Siek and Philip Wadler},
title = {Theorems for Free for Free: Parametricity, With and Without Types},
booktitle = icfp17,
year = {2017},
}
@inproceedings{igarashipoly17,
author = {Yuu Igarashi and Taro Sekiyama and Atsushi Igarashi},
title = {On Polymorphic Gradual Typing},
booktitle = icfp17,
year = {2017},
}
@inproceedings{igarashisession17,
author = {Atsushi Igarashi and Peter Thiemann and Vasco Vasconcelos and Philip Wadler},
title = {Gradual Session Types},
booktitle = icfp,
year = {2017},
}
@Inbook{freyd91,
author="Freyd, Peter",
editor="Carboni, Aurelio and Pedicchio, Maria Cristina and Rosolini, Guiseppe",
title="Algebraically complete categories",
bookTitle="Category Theory: Proceedings of the International Conference held in Como, Italy, July 22--28, 1990",
year="1991",
pages="95--104",
}
@inproceedings{siek-taha07,
 author = "Jeremy G. Siek and Walid Taha",
 title = "Gradual Typing for Objects",
 booktitle = ecoop,
 year = 2007,
}
@article{plotkin1993logic,
  title={A logic for parametric polymorphism},
  author={Plotkin, Gordon and Abadi, Mart{\'\i}n},
  journal={Typed Lambda Calculi and Applications},
  pages={361--375},
  year={1993},
}
@inproceedings{lehmann17,
 author = {Lehmann, Nico and Tanter, \'{E}ric},
 title = {Gradual Refinement Types},
 booktitle = popl,
 year={2017},
} 
@article{felleisen-hieb,
    author = "Matthias Felleisen and Robert Hieb",
    title = "A Revised Report on the Syntactic Theories of Sequential Control and State",
    journal = "Theor. Comput. Sci.",
    volume = "103",
    number = "2",
    pages = "235--271",
    year = "1992",
}
@article{kock95,
title = "Monads for which structures are adjoint to units",
journal = "Journal of Pure and Applied Algebra",
volume = "104",
number = "1",
pages = "41 - 59",
year = "1995",
author = "Anders Kock",
}

@inproceedings{dagand16,
 author = {Dagand, Pierre-Evariste and Tabareau, Nicolas and Tanter, \'{E}ric},
 title = {Partial Type Equivalences for Verified Dependent Interoperability},
 booktitle = icfp,
 year = {2016},
 location = {Nara, Japan},
}

@book{Lambek:1986,
 author = {Lambek, J. and Scott, P. J.},
 title = {Introduction to Higher Order Categorical Logic},
 year = {1986},
 isbn = {0-521-24665-2},
 publisher = {Cambridge University Press},
} 

@article{crutwell-shulman,
Author = {G. S. H. Cruttwell and Michael A. Shulman},
Title = {A unified framework for generalized multicategories},
Year = {2009},
Eprint = {arXiv:0907.2460},
journal = {Theory and Applications of Categories},
volume = {24},
number = {21}
}

@article{wand79ocat,
title = "Fixed-point constructions in order-enriched categories",
journal = "Theoretical Computer Science",
volume = "8",
number = "1",
pages = "13 - 30",
year = "1979",
note = "",
author = "Mitchell Wand"
}

@phdthesis{Dunphy:2002,
 author = {Dunphy, Brian Patrick},
 advisor = {Reddy, Uday},
 title = {Parametricity As a Notion of Uniformity in Reflexive Graphs},
 year = {2002},
 isbn = {0-493-89955-3},
 publisher = {University of Illinois at Urbana-Champaign},
 address = {Champaign, IL, USA},
}

@article{ohearn95,
author = "O'Hearn, Peter W. and Tennent, Robert D.",
title = "Parametricity and Local Variables",
journal = jacm,
volume = "42",
number = "3",
pages = "658--709",
month = "May",
year = "1995"}

@InProceedings{johann15bifibrational,
  title =       {Bifibrational Functorial Semantics for Parametric Polymorphism},
  author =        {Neil Ghani and Patricia Johann and Fredrik Nordvall Forsberg and Federico Orsanigo and Tim Revell},
  booktitle = { Proceedings of Mathematical Foundations of Program Semantics},
  year = {2015}
}

@book{constable+86nuprl-book,
  author =    "Robert L. Constable and Stuart F. Allen and H. M. Bromley and 
               W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and 
               T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and
               Scott F. Smith",
  title="Implementing Mathematics with the {NuPRL} Proof Development System",
  publisher={Prentice Hall},
  year=1986
}

@unpublished{dagand:hal-01629909,
  TITLE = {{Foundations of Dependent Interoperability}},
  AUTHOR = {Dagand, Pierre-Evariste and Tabareau, Nicolas and Tanter, {\'E}ric},
  URL = {https://hal.inria.fr/hal-01629909},
  NOTE = {working paper or preprint},
  YEAR = {2017},
}

@inproceedings{statonlevy13,
 author = {Staton, Sam and Levy, Paul Blain},
 title = {Universal Properties of Impure Programming Languages},
 booktitle = popl,
 year = 2013
}

@inproceedings{seely1984locally,
  title={Locally cartesian closed categories and type theory},
  author={Seely, Robert AG},
  booktitle={Mathematical proceedings of the Cambridge philosophical society},
  volume={95},
  number={1},
  pages={33--48},
  year={1984},
  organization={Cambridge University Press}
}

@inproceedings{hofmann1994interpretation,
  title={On the interpretation of type theory in locally cartesian closed categories},
  author={Hofmann, Martin},
  booktitle={International Workshop on Computer Science Logic},
  pages={427--441},
  year={1994},
}

@article{clairambault2014biequivalence,
  title={The biequivalence of locally cartesian closed categories and Martin-L{\"o}f type theories},
  author={Clairambault, Pierre and Dybjer, Peter},
  journal={Mathematical Structures in Computer Science},
  volume={24},
  number={6},
  year={2014},
  publisher={Cambridge University Press}
}

@article{Vakarthesis,
  author    = {Matthijs V{\'{a}}k{\'{a}}r},
  title     = {In Search of Effectful Dependent Types},
  journal   = {CoRR},
  year      = {2017},
  url       = {http://arxiv.org/abs/1706.07997},
}

@inbook{ahmanghaniplotkin16,
  title     = "Dependent Types and Fibred Computational Effects",
  author    = "Daniel Ahman and Neil Ghani and Plotkin, {Gordon D.}",
  year      = "2016",
  doi       = "10.1007/978-3-662-49630-5_3",
  booktitle = "Foundations of Software Science and Computation Structures",
}
@inproceedings{ahmed08:paramseal,
title = "Parametric polymorphism through run-time sealing, or, Theorems for low, low prices!",
author = "Jacob Matthews and Amal Ahmed",
booktitle = esop,
year = 2008,
month = mar,
location = "Budapest, Hungary",
}
@phdthesis{levy01:phd,
author = "Levy, Paul Blain",
title = "Call-by-Push-Value",
type = "{Ph.~D.} Dissertation",
school = "Queen Mary, University of London",
department = "Department of Computer Science",
address = "London, UK",
month = mar,
year = "2001"}

@inproceedings{neis09,
 author = {Georg Neis and Derek Dreyer and Andreas Rossberg},
 title = {Non-Parametric Parametricity},
 booktitle = icfp,
 pages = "135--148",
 year = {2009},
 month = sep
}

@Article{moggi91,
  author =       {Eugenio Moggi},
  title =        {Notions of computation and monads},
  journal =      {Inform. And Computation},
  year =         {1991},
  volume =    {93},
  number =    {1},
}
 @inproceedings{Wolff:2011:GT,
 author = {Wolff, Roger and Garcia, Ronald and Tanter, \'{E}ric and Aldrich, Jonathan},
 title = {Gradual Typestate},
 booktitle = {Proceedings of the 25th European Conference on Object-oriented Programming},
 series = {ECOOP'11},
 year = {2011},
}

@article{extended,
  author    = {Max S. New and
               Daniel R. Licata},
  title     = {Call-by-name Gradual Type Theory},
  journal   = {CoRR},
  year      = {2018},
  url       = {http://arxiv.org/abs/1802.00061},
}

@article{newlicata2018-fscd,
  author    = {Max S. New and
               Daniel R. Licata},
  title     = {Call-by-name Gradual Type Theory},
  journal   = {FSCD},
  year      = {2018},
}

@article{martinlof83sienna,
	year = {1983/1996},
	journal = {Nordic Journal of Philosophical Logic},
	publisher = {Scandinavian University Press},
	volume = {1},
	author = {Per Martin{-}L\"of},
	number = {1},
	title = {On the Meanings of the Logical Constants and the Justifications of the Logical Laws (Sienna Lectures)},
	pages = {11--60}
}

@Article{pfenningdavies,
    author = {Frank Pfenning and Rowan Davies},
    title = {A Judgmental Reconstruction of Modal Logic},
    journal = {Mathematical Structures in Computer Science},
    year = {2001},
    volume = {11}, 
    pages = {511-540},
}

@article{dagand18,
  title={Foundations of dependent interoperability},
  volume={28},
  DOI={10.1017/S0956796818000011},
  journal={Journal of Functional Programming},
  publisher={Cambridge University Press},
  author={Dagand, Pierr-\'{E}variste and Tabareau, Nicolas and Tanter, \'{E}ric},
  year={2018},
  pages={e9}
}
  
@inproceedings{thatte90,
 author = "Satish Thatte",
 title = "Quasi-static typing",
 booktitle = popl,
 pages = "367--381",
 year = 1990
}

@misc{hejlsberg12,
	Author = {Anders Hejlsberg},
	Date-Added = {2014-01-06 15:39:32 +0000},
	Date-Modified = {2014-09-11 10:40:22 +0000},
	Howpublished = {Microsoft Channel 9 Blog},
	Title = {Introducing {TypeScript}},
	Year = {2012}}

@incollection{bierman14,
	Author = {Bierman, Gavin and Abadi, Mart{\'\i}n and Torgersen, Mads},
	Booktitle = {ECOOP 2014 -- Object-Oriented Programming},
	Date-Added = {2014-10-06 15:02:06 +0000},
	Date-Modified = {2015-11-06 03:05:46 +0000},
	Editor = {Jones, Richard},
	Language = {English},
	Pages = {257-281},
	Publisher = {Springer Berlin Heidelberg},
	Series = {Lecture Notes in Computer Science},
	Title = {Understanding {TypeScript}},
	Volume = {8586},
	Year = {2014}}

@inproceedings{verlaguet13,
	Author = {Julien Verlaguet},
	Booktitle = {Commercial Users of Functional Programming (CUFP)},
	Date-Added = {2014-01-06 15:28:27 +0000},
	Date-Modified = {2014-04-14 11:23:23 +0000},
	Title = {Facebook: Analyzing {PHP} statically},
	Year = {2013}}

@url{chaudhuri14,
	Author = {Avik Chaudhuri},
	Date-Added = {2015-07-16 16:32:06 +0000},
	Date-Modified = {2015-11-18 04:29:52 +0000},
	Keywords = {gradual typing},
	Title = {Flow: a static type checker for JavaScript},
	Url = {http://flowtype.org/},
	Urldate = {2014},
	Year = {2014},
	Bdsk-Url-1 = {http://flowtype.org/}}

@manual{bracha11,
	Author = {Gilad Bracha},
	Date-Added = {2014-04-14 10:26:35 +0000},
	Date-Modified = {2014-04-14 10:27:35 +0000},
	Month = {October},
	Organization = {Google},
	Title = {Optional Types in {Dart}},
	Year = {2011}}

@misc{hejlsberg10,
	Author = {Anders Hejlsberg},
	Date-Added = {2014-01-06 15:43:48 +0000},
	Date-Modified = {2014-01-06 16:09:03 +0000},
	Howpublished = {Microsoft Channel 9 Blog},
	Month = {April},
	Title = {C\# 4.0 and beyond by Anders Hejlsberg},
	Year = {2010}}

@Misc{turner14:typescript,
  author = 	 {Jonathan Turner},
  title = 	 {TypeScript and the Road to 2.0},
  Url = {https://blogs.msdn.microsoft.com/typescript/2014/10/22/typescript-and-the-road-to-2-0/},
  month = 	 {October},
  year = 	 2014}

@inproceedings{siek15:mono,
 author = {Siek, Jeremy G. and Vitousek, Michael M. and Cimini, Matteo and Tobin-Hochstadt, Sam and Garcia, Ronald},
 title = {Monotonic References for Efficient Gradual Typing},
 booktitle = {Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 9032},
 year = {2015},
}

@misc{hack14:blog,
 author = {Julien Verlaguet and Alek Menghrajani},
 title  = {Hack: a new programming language for HHVM},
 url = {https://code.facebook.com/posts/264544830379293/hack-a-new-programming-language-for-hhvm/},
 month = {March},
 year  = {2014}
}

@inproceedings{gronski06,
 author = "Jessica Gronski and Kenneth Knowles and Aaron Tomb and Stephen N. Freund and Cormac Flanagan",
 title = "Sage: Hybrid Checking for Flexible Specifications",
 booktitle = scheme,
 month = sep,
 pages = "93--104",
 year = 2006
}

@inproceedings{Ina:2011zr,
	Author = {Ina, Lintaro and Igarashi, Atsushi},
	Booktitle = {Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications},
	Date-Added = {2012-11-09 23:27:38 +0000},
	Date-Modified = {2012-12-20 08:58:22 -0700},
	Keywords = {dynamic types, generics, gradual typing},
	Series = {OOPSLA '11},
	Title = {Gradual typing for generics},
	Year = {2011}}

@inproceedings{swamy14,
author    = {Nikhil Swamy and C{\'e}dric Fournet and Aseem Rastogi and
  Karthikeyan Bhargavan and Juan Chen and Pierre-Yves Strub and Gavin M. Bierman},
title     = {Gradual typing embedded securely in {J}ava{S}cript},
booktitle = popl14,
year      = {2014},
pages     = {425-438}
}

@article{Allende:2013aa,
	Author = {Esteban Allende and Oscar Calla{\'u} and Johan Fabry and {\'E}ric Tanter and Marcus Denker},
	Date-Added = {2014-03-29 03:55:17 +0000},
	Date-Modified = {2014-03-29 03:55:20 +0000},
	Journal = {Science of Computer Programming},
	Month = aug,
	Note = {Available online},
	Publisher = {Elsevier},
	Title = {Gradual Typing for {Smalltalk}},
	Urldoi = {http://dx.doi.org/10.1016/j.scico.2013.06.006},
	Urlpdf = {http://pleiad.dcc.uchile.cl/papers/2013/allendeAl-scp2013.pdf},
	Users = {eallende , ocallau , jfabry , etanter},
	Year = 2013}

@inproceedings{ahmed06:lr,
title = "Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types",
author = "Amal Ahmed",
booktitle = esop,
year = 2006,
month = mar,
location = "Vienna, Austria",
pages = "69--83"}

@techreport{ahmed06:esop06-techrpt,
author = "Amal Ahmed",
title = "Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types",
institution = "Harvard University",
number = "TR-01-06",
month = jan,
year = 2006,
note="Available at \texttt{http://www.cs.indiana.edu/\linebreak[0]$\sim$amal/\linebreak[0]papers/\linebreak[0]lr-recquant-techrpt.pdf}"}
@inproceedings{ahmed09:sdri,
 author = "Amal Ahmed and Derek Dreyer and Andreas Rossberg",
 title = "State-Dependent Representation Independence",
 booktitle = popl09,
 month = jan,
 year = 2009
}
@article{fuhrmann1999direct,
  title={Direct models of the computational lambda-calculus},
  author={F{\"u}hrmann, Carsten},
  journal={Electronic Notes in Theoretical Computer Science},
  volume={20},
  pages={245--292},
  year={1999},
}

@inproceedings{newahmed18,
author = {Max S. New and Amal Ahmed},
title = {Graduality from Embedding-Projection Pairs},
booktitle = icfp18,
year = {2018},
}

@inproceedings{siek+09designspace,
 author = {Siek, Jeremy and Garcia, Ronald and Taha, Walid},
 title = {Exploring the Design Space of Higher-Order Casts},
 booktitle = esop,
 year = {2009},
 location = {York, UK},
 pages = {17--31},
 numpages = {15},