-
Max S. New authoredMax S. New authored
max.bib 42.50 KiB
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% 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{popl17 = popl # ", Paris, France" }
@STRING{popl18 = popl # ", Los Angeles, California" }
@STRING{popl19 = popl # ", Cascais, Portugal" }
@STRING{popl20 = popl # ", New Orleans, Louisiana" }
% ----
@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{icfp19 = icfp # ", Berlin, Germany" }
% ----
@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{oopsla12 = oopsla # ", Tucson, Arizona" }
% ----
@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},
}
@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{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},
school = {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},
booktitle=popl17,
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=lics00,
year = {2000},
}
@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},
booktitle = popl10,
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},
booktitle =oopsla12,
year = {2012},
}
@inproceedings{XuPJC09,
author = {Xu, Dana N. and Peyton Jones, Simon and Claessen, Koen},
title = {Static Contract Checking for Haskell},
booktitle = 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},
}
@article{newlicataahmed19:extended,
author = {Max S. New and Daniel R. Licata and Amal Ahmed},
title = {Gradual Type Theory (Extend Version)},
year = {2018},
journal = {CoRR},
url = {https://arxiv.org/abs/1811.02440},
}
@inproceedings{newlicataahmed19,
author = {Max S. New and Daniel R. Licata and Amal Ahmed},
title = {Gradual Type Theory},
year = {2019},
booktitle = popl19,
}
@article{newlicata2018,
author = {Max S. New and
Daniel R. Licata},
title = {Call-by-name Gradual Type Theory},
journal = {FSCD},
year = 2018,
}
@article{newlicata2020,
author = {Max S. New and Daniel R. Licata},
title = {Call-by-name Gradual Type Theory},
journal = {LMCS},
year = {2020},
}
@inproceedings{newjamnerahmed20,
author = {Max S. New and Dustin Jamner and Amal Ahmed},
title = {Graduality and Parametricity: Together Again for the First Time},
booktitle = popl20,
year = {2020},
}
@inproceedings{eremonditantergarcia19,
author = {Joseph Eremondi and \`Eric Tanter and Ronald Garcia},
title = { Approximate Normalization for Dependent Gradual Types },
booktitle = icfp19,
year = {2019},
}
@inproceedings{pedrottabareau20,
author={P\'{e}drot, Pierre-Marie and Tabareau, Nicolas},
title = {The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects},
year = {2020},
booktitle = popl20,
}