main.bib

@misc{SWIPrologManual,
  author = "{SWI-Prolog team}",
  title = {{SWI-Prolog} Reference Manual (Section 4.2)},
  year = {2005},
}
  url = "http://www.swi-prolog.org/pldoc/doc_for?object=manual",
  note = "[Online; accessed June 2015]"


@incollection{UrbanN2009,
 author={Christian Urban and Tobias Nipkow},
 title={Nominal verification of algorithm {W}},
 booktitle={From Semantics to Comp. Sci.},
 publisher =	"Cambridge Univ. Press",
 publisher={Cambridge University Press},pages={363--382},year=2009
}
 booktitle={From Semantics to Computer Science. Essays in Honour of Gilles Kahn},
 editor={Y. Bertot and G. Huet and J.-J. L\'evy and G. Plotkin},

@article{NaraschewskiN-JAR,
author={Wolfgang Naraschewski and Tobias Nipkow},
title={Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
journal={Journal of Automated Reasoning},
year=1999,volume=23,pages={299--318}}

@InProceedings{Dubois00,
  title =	"Proving {ML} Type Soundness Within {Coq}",
  author =	"Catherine Dubois",
  bibdate =	"2009-09-29",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/tphol/tphol2000.html#Dubois00",
  booktitle =	"TPHOLs",
  booktitle =	"Theorem Proving in Higher Order Logics, 13th
		 International Conference, {TPHOL}s 2000, Portland,
		 Oregon, {USA}, August 14-18, 2000, Proceedings",
  publisher =	"Springer",
  year = 	"2000",
  volume =	"1869",
  pages =	"126--144",
  series =	"LNCS",
}
  editor =	"Mark Aagaard and John Harrison",
  ISBN = 	"3-540-67863-8",
  series =	"Lecture Notes in Computer Science",
  URL =  	"http://dx.doi.org/10.1007/3-540-44659-1_9",

@article{JFP:185139,
author = {Conor McBride},
title = {First-order unification by structural recursion},
journal = {Journal of Functional Programming},
volume = {13},
issue = {06},
year = {2003},
issn = {1469-7653},
pages = {1061--1075},
numpages = {15},
}
doi = {10.1017/S0956796803004957},
URL = {http://journals.cambridge.org/article_S0956796803004957},

@InProceedings{OutsideInICFP09,
 author = {Schrijvers, Tom and Peyton Jones, Simon and Sulzmann, Martin and Vytiniotis, Dimitrios},
 title = {Complete and Decidable Type Inference for GADTs},
 booktitle = {Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '09},
 year = {2009},
 isbn = {978-1-60558-332-7},
 location = {Edinburgh, Scotland},
 pages = {341--352},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1596550.1596599},
 doi = {10.1145/1596550.1596599},
 acmid = {1596599},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {GADTs, Haskell, type inference},
}

@phdthesis{Ahn14thesis,
  author  = {Ahn, Ki Yung},
  title	  = {The Nax language},
  school  = {Department of Computer Science, Portland State University},
  year	  = 2014,
  month	  = {November},
}
  url = "http://archives.pdx.edu/ds/psu/13198",
  address = {PO Box 751, Portland, OR, 97207 USA},

A prototype implementation of Nax is available at \url{http://github.com/kyagrd/mininax}.

@InProceedings{BirMee98,
  author = "Bird and Meertens",
  title = "Nested Datatypes",
  booktitle = "MPC: 4th International Conference on Mathematics of Program Construction",
  year = "1998",
}
  publisher = "LNCS, Springer-Verlag",

@inproceedings{AhnSheFioPit13,
 author    = {Ki Yung Ahn and Tim Sheard and Marcelo Fiore and Andrew M. Pitts},
 title     = {System {F}i: a Higher-Order Polymorphic Lambda Calculus with Erasable Term Indices},
 booktitle = {TLCA'13},
 year      = {2013},
}
 series    = {TLCA '13},

@inproceedings{AhnShe11,
 author = {Ahn, Ki Yung and Sheard, Tim},
 title = {A hierarchy of {M}endler-style recursion combinators},
 booktitle = {ICFP '11},
 booktitle = {Proceedings of the 16th ACM SIGPLAN international conference on Functional programming},
 year = {2011},
 location = {Tokyo, Japan},
 numpages = {13},
 acmid = {2034807},
 publisher = {ACM},
keywords = {catamorphism, higher-order abstract syntax, histomorphism, parametric polymorphism, parametricity, recursion combinators, recursion schemes, termination, totality},
}
 pages = {234--246},

@InProceedings{AbeMatUus03,
 title = "Generalized Iteration and Coiteration for Higher-Order Nested Datatypes",
 author = "Andreas Abel and Ralph Matthes and Tarmo Uustalu",
 bibdate = "2003-03-04",
 bibsource = "DBLP, http://dblp.uni-trier.de/db/conf/fossacs/fossacs2003.html#AbelMU03",
 booktitle = "FoSSaCS '03",
 booktitle = "Foundations of Software Science and Computational Structures, 6th International Conference, {FOSSACS} 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, {ETAPS} 2003, Warsaw, Poland, April 7-11, 2003, Proceedings",
 year = "2003",
}
 publisher = "Springer",
 volume = "2620",
 pages = "54--69",
 series = "LNCS",
 series = "Lecture Notes in Computer Science",


@PhdThesis{vene00phd,
 author =      "Varmo Vene",
 title =       "Categorical Programming with Inductive and Coinductive Types",
 school =      "Dept.\ of Computer Science, Univ.\ of Tartu",
 month =       aug,
 year =        "2000",
}
 type =        "{PhD} thesis ({Diss.\ Math.\ Univ.\ Tartuensis 23})",

@InProceedings{AbeMat04,
  title =	"Fixed Points of Type Constructors and Primitive
		 Recursion",
  author =	"Andreas Abel and Ralph Matthes",
  bibdate =	"2011-08-04",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/csl/csl2004.html#AbelM04",
  booktitle =	"CSL",
  booktitle =	"Computer Science Logic, 18th International Workshop,
		 {CSL} 2004, 13th Annual Conference of the {EACSL},
		 Karpacz, Poland, September 20-24, 2004, Proceedings",
  publisher =	"Springer",
  year = 	"2004",
  volume =	"3210",
  ISBN = 	"3-540-23024-6",
  pages =	"190--204",
  series =	"LNCS",
  series =	"Lecture Notes in Computer Science",
  URL =  	"http://dx.doi.org/10.1007/978-3-540-30124-0_17",
}

@InProceedings{DegtyarevV95,
  title =	"Simultaneous Regid {E}-Unification Is Undecidable",
  author =	"Anatoli Degtyarev and Andrei Voronkov",
  publisher =	"Springer",
  year = 	"1995",
  volume =	"1092",
  bibdate =	"2009-09-22",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/csl/csl95.html#DegtyarevV95",
  booktitle =	"CSL",
  pages =	"178--190",
  series =	"LNCS",
}
  ISBN = 	"3-540-61377-3",
  series =	"Lecture Notes in Computer Science",
  editor =	"Hans Kleine B{\"u}ning",
  URL =  	"http://dx.doi.org/10.1007/3-540-61377-3_38",
  crossref =	"conf/csl/1995",

@PhdThesis{matthes98phd,
 author = "Ralph Matthes",
 title = "Extensions of System {F} by Iteration and Primitive Recursion on Monotone Inductive Types",
 school = "Ludwig-Maximilians Univ.",
 year = "1998",
 pdf = "http://www.irit.fr/~Ralph.Matthes/dissertation/matthesdiss.pdf",
}
 month = may,
 school = "Ludwig-Maximilians Universit{\"a}t",


@article{HMX99,
 author = {Odersky, Martin and Sulzmann, Martin and Wehr, Martin},
 title = {Type Inference with Constrained Types},
 journal = {Theor. Pract. Object Syst.},
 issue_date = {Jan. 1999},
 volume = {5},
 number = {1},
 month = jan,
 year = {1999},
 issn = {1074-3227},
 pages = {35--55},
 numpages = {21},
 acmid = {308203},
 publisher = {John Wiley \& Sons, Inc.},
 address = {New York, NY, USA},
}
 doi = {10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4},
 url = {http://dx.doi.org/10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4},



@InProceedings{tyinferCHR02,
  author =	"Sandra Alves and Mario Florido",
  title =	"Type Inference using {C}onstraint {H}andling {R}ules",
  keywords =	"type systems",
  pages =	"56--72",
  booktitle =	"{WFLP'01}",
  booktitle =	"{WFLP} '01: Proc.\ 10th Intl.\ Workshop on Functional
		 and (Constraint) Logic Programming, Selected Papers",
  year = 	"2002",
  series =	"{Electr.}\;Notes\;in\;TCS",
  series =	"Electronic Notes in Theoretical Computer Science",
  volume =	"64",
  publisher =	"Elsevier",
}
  month =	nov,
  editor =	"M. Hanus",

@PhdThesis{girard72thesis,
  author = 	 {Jean-Yves Girard},
  title = 	 {Interpr\'etation fonctionelle et \'elimination des coupures de l'arithm\'etique d'ordre sup\'erieur},
  school = 	 {Universit\'e Paris VII},
  year = 	 {1972},
}

@article{Barendregt91,
  author    = {Henk Barendregt},
  title     = {Introduction to Generalized Type Systems},
  journal   = {J. Funct. Program.},
  volume    = {1},
  number    = {2},
  pages     = {125--154},
  year      = {1991},
}



@InProceedings{JonesTHiH99,
	author =	"Mark P. Jones",
	title =	"Typing {Haskell} in {Haskell}",
	booktitle =	"Haskell '99",
	year = 	"1999",
	month =	oct,
}
	booktitle =	"ACM Haskell Workshop {\rm, informal proceedings}",

@Book{AILogTextBook,
	title =	"Artificial Intelligence - Foundations of Computational Agents",
	author =	"David Poole and Alan K. Mackworth",
	publisher =	"Cambridge University Press",
	year = 	"2010",
	bibdate =	"2011-02-04",
	pages =	"I--XVII, 1--662",
}
	ISBN = 	"978-0-521-51900-7",
	URL =  	"http://www.cambridge.org/uk/catalogue/catalogue.asp?isbn=9780521519007",




@InProceedings{AnconaLZ08,
	title =	"Type Inference by Coinductive Logic Programming",
	author =	"Davide Ancona and Giovanni Lagorio and Elena Zucca",
	publisher =	"Springer",
	year = 	"2008",
	volume =	"5497",
	bibdate =	"2009-06-13",
	bibsource =	"DBLP,
	http://dblp.uni-trier.de/db/conf/types/types2008.html#AnconaLZ08",
	booktitle =	"TYPES",
	editor =	"Stefano Berardi and Ferruccio Damiani and Ugo
	de'Liguoro",
	pages =	"1--18",
	series =	"LNCS",
	URL =  	"http://dx.doi.org/10.1007/978-3-642-02444-3",
}
	ISBN = 	"978-3-642-02443-6",
	series =	"Lecture Notes in Computer Science",
	crossref =	"conf/types/2008",


@inproceedings{AL-ECOOP09,
  author = "Davide Ancona and Giovanni Lagorio",
  title = {Coinductive type systems for object-oriented languages},
  booktitle = {ECOOP '09},
  booktitle = {ECOOP 2009 - Object-Oriented Programming},
  abstract = {We propose a novel approach based on coinductive logic
                   to specify type systems of programming languages. The
                   approach consists in encoding programs in Horn formulas
                   which are interpreted w.r.t. their coinductive Herbrand
                   model. We illustrate the approach by first specifying a
                   standard type system for a small object-oriented
                   language similar to Featherweight Java. Then we define
                   an idealized type system for a variant of the language
                   where type annotations can be omitted. The type system
                   involves infinite terms and proof trees not
                   representable in a finite way, thus providing a
                   theoretical limit to type inference of object-oriented
                   programs, since only sound approximations of the system
                   can be implemented. Approximation is naturally captured
                   by the notions of subtyping and subsumption; indeed,
                   rather than increasing the expressive power of the
                   system, as it usually happens, here subtyping is needed
                   for approximating infinite non regular types and proof
                   trees with regular ones. },
  keywords = {objects,types,coinduction},
  year = 2009
}
  publisher = {Springer Verlag},
  volume = {5653}, series = {LNCS}, pages = {2--26},
  editor = {{S. Drossopoulou}},
  series = {Lecture Notes in Computer Science},
  url = {ftp://ftp.disi.unige.it/person/AnconaD/ECOOP09.pdf},


@InProceedings{nadathur99cade,
  author =	"Gopalan Nadathur and Dustin J. Mitchell",
  title =	"System Description: {Teyjus} --- {A} Compiler and
		 Abstract Machine Based Implementation of {$\lambda$Prolog}",
  pages =	"287--291",
  booktitle =	"CADE '99",
  booktitle =	"16th Conf.\ on Automated Deduction (CADE)",
  year = 	"1999",
  series =	"LNAI",
  number =	"1632",
  publisher =	"Springer",
}
  address =	"Trento",
  editor =	"H. Ganzinger",

@InProceedings{cheney04iclp,
  author =	"James Cheney and Christian Urban",
  title =	"{$\alpha$P}rolog: A Logic Programming Language with
		 Names, Binding, and $\alpha$-Equivalence",
  year = 	"2004",
  booktitle =	"ICLP '04",
  booktitle =	"Logic Programming, 20th International Conference",
  publisher =	"Springer",
}
  pages =	"269--283",
  volume =	"3132",
  series =	"LNCS",
  booktitle =	"Logic Programming, 20th International Conference",
  editor =	"Bart Demoen and Vladimir Lifschitz",

@article{SchDemDesWei13,
  author = {Tom Schrijvers and Bart Demoen and Benoit Desouter and Jan Wielemaker},
  title = {Delimited Continuations for Prolog},
  year = {2013},
  journal = {TPLP},
  journal = {Theory and Practice of Logic Programming (TPLP)},
  note = {Proceedings of ICLP'13},
  abstract = {Delimited continuations are a famous control primitive that originates in the functional programming world. It allows the programmer to suspend and capture the remaining part of a computation in order to resume it later. We put a new Prolog-compatible face on this primitive and specify its semantics by means of a meta-interpreter. Moreover, we establish the power of delimited continuations in Prolog with several example definitions of high-level language features. Finally, we show how to easily and effectively add delimited continuations support to the WAM.},
}
  publisher = {Cambridge University Press},
  url = {/Research/papers/iclp2013.pdf},

@article{iclp2013,
  author = {Tom Schrijvers and Bart Demoen and Benoit Desouter and Jan Wielemaker},
  title = {Delimited Continuations for Prolog},
  year = {2013},
  publisher = {Cambridge University Press},
  journal = {Theory and Practice of Logic Programming (TPLP)},
  note = {Proceedings of the International Conference on Logic Programming (ICLP)},
  url = {/Research/papers/iclp2013.pdf},
  abstract = {Delimited continuations are a famous control primitive that originates in the functional programming world. It allows the programmer to suspend and capture the remaining part of a computation in order to resume it later. We put a new Prolog-compatible face on this primitive and specify its semantics by means of a meta-interpreter. Moreover, we establish the power of delimited continuations in Prolog with several example definitions of high-level language features. Finally, we show how to easily and effectively add delimited continuations support to the WAM.},
}

@TECHREPORT{Gaster96apolymorphic,
    author = {Benedict R. Gaster and Mark P. Jones},
    title = {A Polymorphic Type System for Extensible Records and Variants},
    institution = {},
    year = {1996}
}


@InProceedings{microKanren,
  title =	"{$\mu$Kanren}: A Minimal Functional Core for Relational Programming ",
  booktitle =	"Scheme '13",
  author =	"Jason Hemann and Daniel P. Friedman",
  year = 2013,
}
  booktitle =	"Proceedings of the annual Workshop on Scheme and Functional Programming",
  series = {Scheme '13},
  URL =  	"http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf",


@InProceedings{SRLP15,
  title =	"Structural Resolution for Logic Programming",
  author =	"Patricia Johann and Ekaterina Komendantskaya and Vladimir Komendantskiy",
  booktitle =	"Techincal Communications of {ICLP}",
  year = 2015,
}

@InProceedings{PCR15,
  title =	"A Type Theoretic Approach to Structural Resolution",
  author =	"Peng Fu and Ekaterina Komendantskaya",
  booktitle =	"pre-Proceedings of LOPSTR'15",
  year = 2015,
}

@Article{PerWar80,
  author =      "Fernando C. N. Pereira and David H. D. Warren",
  title =       "Definite clause grammars for language analysis",
  journal =     "Artificial Intelligence",
  year =        "1980",
  volume =      "13",
  pages =       "231--278",
}

@Book{ReasonedSchemer,
  title =	"The Reasoned Schemer",
  author =	"Daniel P. Friedman and William E. Byrd and Oleg Kiselyov",
  publisher =	"MIT Press",
  year = 	"2005",
  bibdate =	"2011-04-06",
  ISBN = 	"978-0-262-56214-0",
  pages =	"I--X, 1--169",
}

@PhdThesis{miniKanrenThesis,
  title =	"Relational Programming in miniKanren: Techniques,
		 Applications, and Implementations",
  author =	"William E. Byrd",
  publisher =	"[Bloomington, Ind.] : Indiana Universtiy",
  year = 	"2009",
  abstract =	"The promise of logic programming is that programs can
		 be written {\it relationally}, without distinguishing
		 between input and output arguments. Relational programs
		 are remarkably flexible---for example, a relational
		 type-inferencer also performs type checking and type
		 inhabitation, while a relational theorem prover
		 generates theorems as well as proofs and can even be
		 used as a simple proof assistant. Unfortunately,
		 writing relational programs is difficult, and requires
		 many interesting and unusual tools and techniques. For
		 example, a relational interpreter for a subset of
		 Scheme might use nominal unification to support
		 variable binding and scope, Constraint Logic
		 Programming over Finite Domains (CLP(FD)) to implement
		 relational arithmetic, and tabling to improve
		 termination behavior. In this dissertation I present
		 {\it miniKanren}, a family of languages specifically
		 designed for relational programming, and which supports
		 a variety of relational idioms and techniques. I show
		 how miniKanren can be used to write interesting
		 relational programs, including an extremely flexible
		 lean tableau theorem prover and a novel constraint-free
		 binary arithmetic system with strong termination
		 guarantees. I also present interesting and practical
		 techniques used to implement miniKanren, including a
		 nominal unifier that uses triangular rather than
		 idempotent substitutions and a novel {"}walk{"}-based
		 algorithm for variable lookup in triangular
		 substitutions. The result of this research is a family
		 of languages that supports a variety of relational
		 idioms and techniques, making it feasible and useful to
		 write interesting programs as relations.",
  bibsource =	"OAI-PMH server at scholarworks.iu.edu",
  contributor =  "Daniel P Friedman",
  description =  "Thesis (Ph.D.) - Indiana University, Computer
		 Sciences, 2009",
  language =	"EN",
  oai =  	"oai:https://scholarworks.iu.edu:2022/8777",
  rights =	"This work is licensed under the Creative Commons
		 Attribution-By 3.0 Unported License;
		 http://creativecommons.org/licenses/by/3.0/",
  school =	"Indiana University",
  school =	"Indiana University, Computer Sciences, 2009",
  subject =	"relational programming; miniKanren; logic programming;
		 Scheme; Computer Science",
}
  URL =  	"http://hdl.handle.net/2022/8777",


@Misc{Scott69,
  author =	"Dana S. Scott",
  title =	"A type--theoretic alternative to {CUCH} {ISWIM}
		 {OWHY}",
  howpublished = "Manuscript",
  year = 	"1969",
}

@InProceedings{CsorbaCHRforTyInf12,
  author =	"J\'anos Csorba and Zsolt Zombori and P\'eter Szeredi",
  title =	"Pros and Cons of Using {CHR} for Type Inference",
  booktitle =	"CHR'12",
  booktitle =	"{CHR} '12: Proc.\ 9th Workshop on Constraint Handling
		 Rules",
  year = 	"2012",
  series =	"KU Leuven, Dept. of CS, Tech-report CW 624",
  abstract =	"We report on using logic programming and in particular
		 the Constraint Handling Rules extension of Prolog to
		 provide static type analysis for the Q functional
		 language. We discuss some of the merits and
		 difficulties of CHR that we came across during
		 implementation of a type inference tool.",
  keywords =	"type systems",
  pdf =  	"http://dtai.cs.kuleuven.be/CHR/papers/
		 chr2012/02-Csorba-chr12.pdf",
}
  month =	sep,
  pages =	"16--31",
  editor =	"Jon Sneyers and Thom Fr{\"u}hwirth",
  publisher =	"K.U.Leuven, Department of Computer Science , Technical
		 report CW 624",


@InProceedings{SchrijversCWD08,
  title =	"Towards Typed Prolog",
  author =	"Tom Schrijvers and V{\'i}tor Santos Costa
	 	 and Jan Wielemaker and Bart Demoen",
  bibdate =	"2008-12-17",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/iclp/iclp2008.html#SchrijversCWD08",
  booktitle =	"ICLP'08",
  booktitle =	"Logic Programming, 24th International Conference,
		 {ICLP} 2008, Udine, Italy, December 9-13 2008,
		 Proceedings",
  publisher =	"Springer",
  year = 	"2008",
  volume =	"5366",
  pages =	"693--697",
  series =	"LNCS",
  series =	"Lecture Notes in Computer Science",
}
  ISBN = 	"978-3-540-89981-5",
  editor =	"Maria Garcia de la Banda and Enrico Pontelli",
  URL =  	"http://dx.doi.org/10.1007/978-3-540-89982-2",


@inproceedings{GPH2012,
 author = {Yorgey, Brent A. and Weirich, Stephanie and Cretin, Julien and Peyton Jones, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos{\'e} Pedro},
 title = {Giving {Haskell} a Promotion},
 booktitle = {TLDI '12},
 booktitle = {Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation},
 year = {2012},
 numpages = {14},
 acmid = {2103795},
 publisher = {ACM},
 keywords = {haskell, kinds, polymorphism, promotion},
} 
 pages = {53--66},
 series = {TLDI '12},
 url = {http://doi.acm.org/10.1145/2103786.2103795},
 doi = {10.1145/2103786.2103795},
 isbn = {978-1-4503-1120-5},
 location = {Philadelphia, Pennsylvania, USA},
 address = {New York, NY, USA},


@InProceedings{Despeyroux84,
  title =	"Executable Specification of Static Semantics",
  author =	"Thierry Despeyroux",
  bibdate =	"2011-06-10",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/conf/sdt/sdt1984.html#Despeyroux84",
  booktitle =	"Semantics of Data Types",
  booktitle =	"Semantics of Data Types, International Symposium,
		 Sophia-Antipolis, France, June 27-29, 1984, Proceedings",
  publisher =	"Springer",
  year = 	"1984",
  volume =	"173",
  pages =	"215--233",
  series =	"LNCS",
  series =	"Lecture Notes in Computer Science",
}
  ISBN = 	"3-540-13346-1",
  URL =  	"http://dx.doi.org/10.1007/3-540-13346-1_11",
  editor =	"Gilles Kahn and David B. MacQueen and Gordon D. Plotkin",



@inproceedings{QML09,
 author = {Russo, Claudio V. and Vytiniotis, Dimitrios},
 title = {QML: Explicit First-class Polymorphism for ML},
 booktitle = {ML '09},
 booktitle = {Proceedings of the 2009 ACM SIGPLAN Workshop on ML},
 year = {2009},
 pages = {3--14},
 numpages = {12},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {impredicativity, polymorphism, type inference},
} 
 series = {ML '09},
 acmid = {1596630},
 location = {Edinburgh, Scotland},
 isbn = {978-1-60558-509-3},
 doi = {10.1145/1596627.1596630},
 url = {http://doi.acm.org/10.1145/1596627.1596630},