diff --git a/jfp-paper/max.bib b/jfp-paper/max.bib
new file mode 100644
index 0000000000000000000000000000000000000000..f8e9bb248368f8a3dc18862b3e27e5323fe1ceb0
--- /dev/null
+++ b/jfp-paper/max.bib
@@ -0,0 +1,1245 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% 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},
+ publisher = {Springer-Verlag},
+ address = {Berlin, Heidelberg},
+}
+
+
+@Book{levy03cbpvbook,
+ author = {Paul Blain Levy},
+ title = {Call-By-Push-Value: A Functional/Imperative Synthesis},
+ publisher = {Springer},
+ year = {2003}
+}
+
+
+@InProceedings{bauerpretnar13eff,
+author="Bauer, Andrej and Pretnar, Matija",
+title="An Effect System for Algebraic Effects and Handlers",
+booktitle="Algebra and Coalgebra in Computer Science",
+year="2013",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="1--16",
+}
+
+@inproceedings{lindley+17frank,
+ author = {Lindley, Sam and McBride, Conor and McLaughlin, Craig},
+ title = {Do Be Do Be Do},
+ booktitle = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
+ series = {POPL 2017},
+ year = {2017},
+ location = {Paris, France},
+ pages = {500--514},
+ numpages = {15},
+ publisher = {ACM},
+}
+
+@InProceedings{munchmaccagnoni14nonassociative,
+author="Munch-Maccagnoni, Guillaume",
+title="Models of a Non-associative Composition",
+booktitle="Foundations of Software Science and Computation Structures",
+year="2014",
+pages="396--410",
+}
+
+@article{girard01locussolum,
+ title={Locus Solum: From the rules of logic to the logic of rules},
+ volume={11},
+ number={3},
+ journal={Mathematical Structures in Computer Science},
+ publisher={Cambridge University Press},
+ author={Girard, Jean-Yves},
+ year={2001},
+ pages={301–506 }}
+
+@PhdThesis{zeilberger09thesis,
+ author = {Noam Zeilberger},
+ title = {The Logical Basis of Evaluation Order and Pattern-Matching. },
+ school = {Carnegie Mellon University},
+ year = {2009},
+}
+
+@Article{siekth16recursiveunion,
+ author = {Jeremy Siek and Sam Tobin-Hochstadt},
+ title = {The recursive union of some gradual types},
+ journal = {A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Springer LNCS)},
+ year = {2016},
+ volume = {volume 9600},
+}
+
+@article{igarashi+17gradualsession,
+ author = {Igarashi, Atsushi and Thiemann, Peter and Vasconcelos, Vasco T. and Wadler, Philip},
+ title = {Gradual Session Types},
+ journal = {Proceedings of ACM Programning Languages},
+ issue_date = {September 2017},
+ volume = {1},
+ number = {ICFP},
+ month = aug,
+ year = {2017},
+ pages = {38:1--38:28},
+ articleno = {38},
+ numpages = {28},
+}
+
+@InProceedings{pfenninggriffith15session,
+ author = {Frank Pfenning and Dennis Griffith},
+ title = {Polarized Substructural Session Types (invited talk)},
+ booktitle = {International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)},
+ year = {2015}
+}
+
+@inproceedings{siekwadler10zigzag,
+ author = {Siek, Jeremy G. and Wadler, Philip},
+ title = {Threesomes, with and Without Blame},
+ booktitle = popl,
+ year = {2010},
+ location = {Madrid, Spain},
+ pages = {365--376},
+ publisher = {ACM}
+}
+
+@inproceedings{plotkinabadi93,
+ author = {Gordon D. Plotkin and Mart{\'{\i}}n Abadi},
+ title = {A Logic for Parametric Polymorphism},
+ booktitle = {Typed Lambda Calculi and Applications, International Conference on
+ Typed Lambda Calculi and Applications, {TLCA} '93, Utrecht, The Netherlands,
+ March 16-18, 1993, Proceedings},
+ pages = {361--375},
+ year = {1993},
+}
+
+@phdthesis{dunphyphd,
+ author = {Dunphy, Brian Patrick},
+ advisor = {Reddy, Uday},
+ title = {Parametricity As a Notion of Uniformity in Reflexive Graphs},
+ year = {2002},
+ publisher = {University of Illinois at Urbana-Champaign},
+ address = {Champaign, IL, USA},
+}
+
+@inproceedings{vitousekswordssiek:2017,
+ author = {Vitousek, Michael M. and Swords, Cameron and Siek, Jeremy G.},
+ title = {Big Types in Little Runtime: Open-world Soundness and Collaborative Blame for Gradual Type Systems},
+ series = {POPL 2017},
+ year = {2017},
+}
+
+@inproceedings{greenmanfelleisen:2018,
+ author = {Greenman, Ben and Felleisen, Matthias},
+ title = {A Spectrum of Type Soundness and Performance},
+ booktitle = icfp18,
+ year = {2018}
+}
+
+@inproceedings{nakano,
+ title={A modality for recursion},
+ author={Nakano, Hiroshi},
+ booktitle={Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on},
+}
+@inproceedings{levy17popl,
+ author = {Levy, Paul Blain},
+ title = {Contextual Isomorphisms},
+ booktitle = popl,
+ year={2017},
+}
+
+@article{herman2010spaceefficient,
+ title={Space-efficient gradual typing},
+ author={Herman, David and Tomb, Aaron and Flanagan, Cormac},
+ journal={Higher-Order and Symbolic Computation},
+ year={2010},
+}
+
+@inproceedings{greenberg15spaceefficient,
+ author = {Greenberg, Michael},
+ title = {Space-Efficient Manifest Contracts},
+ booktitle = popl,
+ year = {2015},
+ location = {Mumbai, India},
+ pages = {181--194},
+}
+
+
+@article{dagand+18interoperability,
+title={Foundations of dependent interoperability},
+volume={28}, DOI={10.1017/S0956796818000011},
+journal={Journal of Functional Programming},
+publisher={Cambridge University Press},
+author={Dagand, Pierre-\`Evariste and Tabareau, Nicolas and Tanter, \`Eric},
+year={2018},
+pages={e9}}
+
+@InProceedings{ahman+16fiberedeffects,
+author="Ahman, Danel and Ghani, Neil and Plotkin, Gordon D.",
+title="Dependent Types and Fibred Computational Effects",
+booktitle="Foundations of Software Science and Computation Structures",
+year="2016",
+pages="36--54",
+}
+
+@article{andreoli92focus,
+ author = {Jean-Marc Andreoli},
+ title = {Logic programming with focusing proofs in linear logic},
+ journal = {Journal of Logic and Computation},
+ year = {1992},
+ volume = 2,
+ number = 3,
+ pages = {297--347},
+}
+@inproceedings{greenberg-manifest,
+ author = {Greenberg, Michael and Pierce, Benjamin C. and Weirich, Stephanie},
+ title = {Contracts Made Manifest},
+ series = {POPL '10},
+ year = 2010
+}
+
+@article{Degen2012TheIO,
+ title={The interaction of contracts and laziness},
+ author={Markus Degen and Peter Thiemann and Stefan Wehr},
+ journal={Higher-Order and Symbolic Computation},
+ year={2012},
+ volume={25},
+ pages={85-125}
+}
+@InProceedings{findlerflattfelleisen04,
+author="Findler, Robert Bruce and Flatt, Matthew and Felleisen, Matthias",
+title="Semantic Casts: Contracts and Structural Subtyping in a Nominal World",
+booktitle= ecoop,
+year={2004}
+}
+
+@inproceedings{chaperonesimpersonators,
+ author = {Strickland, T. Stephen and Tobin-Hochstadt, Sam and Findler, Robert Bruce and Flatt, Matthew},
+ title = {Chaperones and Impersonators: Run-time Support for Reasonable Interposition},
+ series = oopsla,
+ year = {2012},
+}
+
+@inproceedings{XuPJC09,
+ author = {Xu, Dana N. and Peyton Jones, Simon and Claessen, Koen},
+ title = {Static Contract Checking for Haskell},
+ series = popl09,
+ year = {2009},
+}
+
+@InProceedings{hinzeJeuringLoh06,
+author="Hinze, Ralf and Jeuring, Johan and L{\"o}h, Andres",
+title="Typed Contracts for Functional Programming",
+booktitle=flops,
+year="2006",
+}
+
+@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},
+}
+@Unpublished{newlicataahmed19:extended,
+author = {Max S. New and Daniel R. Licata and Amal Ahmed},
+title = {Gradual Type Theory (Extend Version)},
+year = {2018},
+url = {https://arxiv.org/abs/1811.02440},
+}
+