bibliography.bib

@article{Eckhardt2007,
  abstract = {Previous work on semantics-based multi-stage programming (MSP) language design focused on homogeneous designs, where the generating and the generated languages are the same. Homogeneous designs simply add a hygienic quasi-quotation and evaluation mechanism to a base language. An apparent disadvantage of this approach is that the programmer is bound to both the expressivity and performance characteristics of the base language. This paper proposes a practical means to avoid this by providing specialized translations from subsets of the base language to different target languages. This approach preserves the homogeneous ``look'' of multi-stage programs, and, more importantly, the static guarantees about the generated code. In addition, compared to an explicitly heterogeneous approach, it promotes reuse of generator source code and systematic exploration of the performance characteristics of the target languages.},
  author = {Eckhardt, Jason and Kaiabachev, Roumen and Pasalic, Emir and Swadi, Kedar and Taha, Walid},
  date-added = {2017-05-24 00:21:32 +0000},
  date-modified = {2017-05-24 00:21:32 +0000},
  doi = {10.1007/s00354-007-0020-x},
  issn = {1882-7055},
  journal = {New Generation Computing},
  number = {3},
  pages = {305--336},
  title = {Implicitly Heterogeneous Multi-Stage Programming},
  url = {http://dx.doi.org/10.1007/s00354-007-0020-x},
  volume = {25},
  year = {2007},
  bdsk-url-1 = {http://dx.doi.org/10.1007/s00354-007-0020-x}
}
@inbook{Zook2009,
  address = {Berlin, Heidelberg},
  author = {Zook, David and Pasalic, Emir and Sarna-Starosta, Beata},
  booktitle = {Practical Aspects of Declarative Languages: 11th International Symposium, PADL 2009, Savannah, GA, USA, January 19-20, 2009. Proceedings},
  date-added = {2017-05-24 00:19:27 +0000},
  date-modified = {2017-05-24 00:19:27 +0000},
  doi = {10.1007/978-3-540-92995-6_12},
  editor = {Gill, Andy and Swift, Terrance},
  isbn = {978-3-540-92995-6},
  pages = {168--182},
  publisher = {Springer Berlin Heidelberg},
  title = {Typed Datalog},
  url = {http://dx.doi.org/10.1007/978-3-540-92995-6_12},
  year = {2009},
  bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-92995-6_12}
}
@inproceedings{DBLP:conf/amw/ArefKPV15,
  author = {Molham Aref and Benny Kimelfeld and Emir Pasalic and Nikolaos Vasiloglou},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  biburl = {http://dblp.uni-trier.de/rec/bib/conf/amw/ArefKPV15},
  booktitle = {Proceedings of the 9th Alberto Mendelzon International Workshop on Foundations of Data Management, Lima, Peru, May 6 - 8, 2015.},
  date-added = {2017-05-23 23:37:35 +0000},
  date-modified = {2017-05-23 23:56:17 +0000},
  editor = {Andrea Cali and Maria-Esther Vidal},
  publisher = {CEUR-WS.org},
  timestamp = {Mon, 30 May 2016 16:28:37 +0200},
  title = {Extending Datalog with Analytics in LogicBlox},
  url = {http://ceur-ws.org/Vol-1378/AMW_2015_paper_3.pdf},
  volume = {1378},
  year = {2015},
  bdsk-url-1 = {http://ceur-ws.org/Vol-1378/AMW_2015_paper_3.pdf}
}
@inproceedings{Aref:2015:DIL:2723372.2742796,
  acmid = {2742796},
  address = {New York, NY, USA},
  author = {Aref, Molham and ten Cate, Balder and Green, Todd J. and Kimelfeld, Benny and Olteanu, Dan and Pasalic, Emir and Veldhuizen, Todd L. and Washburn, Geoffrey},
  booktitle = {Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data},
  date-added = {2017-05-23 23:37:02 +0000},
  date-modified = {2017-05-23 23:37:02 +0000},
  doi = {10.1145/2723372.2742796},
  isbn = {978-1-4503-2758-9},
  keywords = {datalog, incremental maintenance, leapfrog triejoin, live programming, logicblox, logiql, predictive analytics, transaction repair},
  location = {Melbourne, Victoria, Australia},
  numpages = {12},
  pages = {1371--1382},
  publisher = {ACM},
  series = {SIGMOD '15},
  title = {Design and Implementation of the LogicBlox System},
  url = {http://doi.acm.org/10.1145/2723372.2742796},
  year = {2015},
  bdsk-url-1 = {http://doi.acm.org/10.1145/2723372.2742796},
  bdsk-url-2 = {http://dx.doi.org/10.1145/2723372.2742796}
}
@inproceedings{SZPA08,
  author = {Beata Sarna-Sarosta and David Zook and Emir Pasalic and Molham Aref},
  booktitle = {Fifth Workshop on Constraint Handling Rules},
  date-added = {2008-06-10 17:02:21 -0400},
  date-modified = {2008-06-10 17:09:52 -0400},
  month = {July},
  title = {Relating Constraint Handling Rules to Datalog},
  year = {2008}
}
@unpublished{PST06,
  author = {Pasalic, Emir and Siek, Jeremy and Taha, Walid},
  date-added = {2006-12-24 02:13:21 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  note = {Unpublished.},
  title = {Concoqtion: Mixing Indexed Types and Hindley-Milner Type Inference},
  url = {http://emirpasalichome.appspot.com/p2/papers/PST06.pdf},
  year = {2006},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/PST06.pdf}
}
@inproceedings{FPST07,
  abstract = {Almost twenty years after the pioneering efforts of Cardelli, the
programming languages community is vigorously pursuing ways to
incorporate  Fomega-style indexed types into programming
languages.  This paper advocates Concoqtion, a practical approach to
adding such highly expressive types to full-fledged programming
languages.  The approach is applied to MetaOCaml using the Coq proof
checker to conservatively extend Hindley-Milner type inference.  The
implementation of MetaOCaml Concoqtion requires minimal modifications
to the syntax, the type checker, and the compiler; and yields a
language comparable in notation to the leading proposals.  The
resulting language provides unlimited expressiveness in the type
system while maintaining decidability.  Furthermore, programmers can
take advantage of a wide range of libraries not only for the
programming language but also for the indexed types.  Programming in
MetaOCaml Concoqtion is illustrated with small examples and a case
study implementing a statically-typed domain-specific language.
},
  author = {Fogarty, Seth and Pasalic, Emir and Siek, Jeremy and Taha, Walid},
  booktitle = {ACM SIGPLAN 2007 Workshop on Partial Evaluation and Program Manipulation (PEPM '07)},
  date-added = {2006-12-22 14:56:44 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  title = {Concoqtion: Indexed Types Now!},
  url = {http://emirpasalichome.appspot.com/p2/papers/FPST07.pdf},
  year = {2007},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/FPST07.pdf}
}
@inproceedings{STKP06,
  author = {Swadi, Kedar and Taha, Walid and Kiselyov, Oleg and Pasalic, Emir},
  booktitle = {Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '06)},
  date-added = {2005-12-19 22:09:52 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  month = {January},
  publisher = {ACM Press},
  title = {A Monadic Approach for Avoiding Code Duplication when Staging Memoized Functions},
  url = {http://emirpasalichome.appspot.com/p2/papers/PEPM06.pdf},
  year = {2006},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/PEPM06.pdf}
}
@inproceedings{EKPST05,
  abstract = {Previous work on semantics-based multi-stage program- 
ming (MSP) language design focused on homogeneous designs, where the 
generating and the generated languages are the same. Homogeneous de- 
signs simply add a hygienic quasi-quotation and evaluation mechanism to 
a base language. An apparent disadvantage of this approach is that the 
programmer is bound to both the expressivity and performance charac- 
teristics of the base language. This paper proposes a practical means to 
avoid this by providing specialized translations from subsets of the base 
language to different target languages. This approach preserves the ho- 
mogeneous ``look'' of multi-stage programs, and, more importantly, the 
static guarantees about the generated code. In addition, compared to an 
explicitly heterogeneous approach, it promotes reuse of generator source 
code and systematic exploration of the performance characteristics of the 
target languages. 

To illustrate the proposed approach, we design and implement a trans- 
lation to a subset of C suitable for numerical computation, and show that 
it preserves static typing. The translation is implemented, and evaluated 
with several benchmarks. The implementation is available in the online 
distribution of MetaOCaml. },
  author = {Eckhardt, Jason and Kaiabachev, Roumen and Pasalic, Emir and Swadi, Kedar and Taha, Walid},
  booktitle = {Proceedings of the 4th ACM International Conference on Generative Programming and Component Engineering (GPCE'05)},
  date-added = {2005-10-27 10:55:18 -0500},
  date-modified = {2007-02-01 13:51:12 -0600},
  month = {September},
  publisher = {Springer-Verlag},
  series = {Lecture Notes In Computer Science},
  title = {Implicitly Heterogeneous Multi-Stage Programming},
  url = {http://emirpasalichome.appspot.com/p2/papers/EKPST05-long.pdf},
  volume = {3676},
  year = {2005},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/EKPST05-long.pdf}
}
@inproceedings{SSDBM097,
  author = {Cushing, Judith Bayard and Laird, Justin and Pasalic, Emir and Kutter, Elizabeth and Hunkapiller, Tim and Zucker, Frank and Yee., David P.},
  booktitle = {Ninth International Conference on Scientific and Statistical Database Management},
  date-added = {2004-12-09 15:20:16 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  publisher = {IEEE Computer Society Press},
  title = {Beyond interoperability - tracking and managing the results of computational applications.},
  year = {1997}
}
@inproceedings{SheardDSL99,
  address = {New York, NY, USA},
  author = {Sheard, Tim and Benaissa, Zine-el-Abidine and Pasalic, Emir},
  booktitle = {Second Conference on Domain-Specific Languages (DSL'99)},
  date-added = {2004-12-09 15:24:40 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  month = {October},
  organization = {USENIX},
  pages = {81--94},
  publisher = {ACM Press},
  title = {DSL implementation using staging and monads},
  url = {http://emirpasalichome.appspot.com/p2/papers/sheard99dsl.pdf},
  year = {1999},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/sheard99dsl.pdf}
}
@inproceedings{ITC01*148,
  author = {Moran, Andrew and Teisher, James and Gill, Andrew and Pasalic, Emir and Veneruso, J.},
  booktitle = {International Test Conference 2001 (ITC '01)},
  date-added = {2004-12-09 15:26:00 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  month = {October},
  organization = {IEEE},
  pages = {148-- 156},
  title = {Automated translation of legacy code for {ATE}.},
  url = {http://emirpasalichome.appspot.com/p2/papers/ITC-00-Translator.pdf},
  year = {2001},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/ITC-00-Translator.pdf}
}
@inproceedings{PTS02,
  abstract = {Multi-stage languages proviide a convenient notation
for explicitly staging programs. Staging a definitional interpreter
for a domain specific language is one way of deriving an
implementation that is both readable and efficient. In an untyped
setting, staging an interpreter ``removes a complete layer of interpretive
overhead'', just like partial evaluation. In a typed setting
however, Hindley-Milner type systems do not allow us to exploit
typing information in the language being interpreted. In practice,
this can have a slowdown cost factor of three or more times.
Previously, both type specialization and tag elimination were applied
to this problem. In this paper we propose an alternative approach,
namely, expressing the definitional interpreter in a dependently
typed programming language. We report on our experience
with the issues that arose in writing such an interpreter and in designing
such a language.
To demonstrate the soundness of combining staging and dependent
types in a general sense, we formalize our language (called
Meta-D) and prove its type safety. To formalize Meta-D, we extend
Shao, Saha, Trifonov and Papaspyrou's !H language to a multilevel
setting. Building on !H allows us to demonstrate type safety
in a setting where the type language contains all the calculus of inductive
constructions, but without having to repeat the work needed
for establishing the soundness of that system.},
  author = {Pasalic, Emir and Sheard, Tim and Taha, Walid},
  booktitle = {The International Conference on Functional Programming (ICFP '02)},
  date-added = {2004-12-09 15:28:46 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  month = {October},
  organization = {ACM},
  publisher = {ACM Press},
  title = {Tagless staged interpreters for typed languages.},
  url = {http://emirpasalichome.appspot.com/p2/papers/TaglessInterp-2.pdf},
  year = {2002},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/TaglessInterp-2.pdf}
}
@inproceedings{PL04,
  abstract = {We present two case studies demonstrating the use of type- 
equality constraints in a meta-language to enforce semantic invariants of 
ob ject-language programs such as scoping and typing rules. We apply this 
technique to several interesting problems, including (1) the construction 
of tagless interpreters; (2) statically checking de Bruijn indices involving 
pattern-based binding constructs; and (3) evolving embedded DSL im- 
plementations to include domain-specific types and optimizations that 
respect those types. 
},
  author = {Pasalic, Emir and Linger, R. Nathan},
  booktitle = {Generative Programming and Component Engineering: Third International Conference},
  date-added = {2004-12-09 15:30:58 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  editor = {Karsai, Gabor and Visser, Eelco},
  month = {October},
  publisher = {Lecture Notes in Computer Science, Springer-Verlag},
  title = {Meta-programming with Typed Object-Language Representations},
  url = {http://emirpasalichome.appspot.com/p2/papers/GPCE04.pdf},
  year = {2004},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/GPCE04.pdf}
}
@inproceedings{PS04,
  abstract = {We report our experience with exploring a new point in the design space for formal 
reasoning systems: the development of the programming language ?mega. ?mega 
is intended as both a practical programming language and a logic. The main goal of 
?mega is to allow programmers to describe and reason about semantic properties of 
programs from within the programming language itself, mainly by using a powerful 
type system. 
We illustrate the main features of ?mega by developing an interesting meta- 
programming example. First, we show how to encode a set of well-typed simply 
typed ?-calculus terms as an ?mega data-type. Then, we show how to implement a 
substitution operation on these terms that is guaranteed by the ?mega type system 
to preserve their well-typedness. 
},
  author = {Sheard, Tim and Pasalic, Emir},
  booktitle = {Logical Frameworks and Meta-Languages workshop. Proceedings.},
  date-added = {2004-12-09 15:40:06 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  title = {Meta-programming With Built-in Type Equality},
  url = {http://emirpasalichome.appspot.com/p2/papers/LFM04.pdf},
  year = {2004},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/LFM04.pdf}
}
@article{1346644,
  address = {Amsterdam, The Netherlands, The Netherlands},
  author = {Tim Sheard and Emir Pasalic},
  date-modified = {2008-04-05 01:39:19 -0400},
  doi = {http://dx.doi.org/10.1016/j.entcs.2007.11.012},
  issn = {1571-0661},
  journal = {Electron. Notes Theor. Comput. Sci.},
  pages = {49--65},
  publisher = {Elsevier Science Publishers B. V.},
  title = {Meta-programming With Built-in Type Equality (journal version)},
  volume = {199},
  year = {2008},
  bdsk-url-1 = {http://dx.doi.org/10.1016/j.entcs.2007.11.012}
}
@phdthesis{P04,
  abstract = {  
  Meta-programming, writing programs that write other programs,
  involves two kinds of languages. The meta-language is the language
  in which meta-programs, which construct or manipulate other
  programs, are written.  The object-language is the language of
  programs being manipulated.
  
  We study a class of meta-language features that are used to write
  meta-programs that are statically guaranteed to maintain semantic
  invariants of object-language programs, such as typing and scoping.
  We use type equality in the type system of the meta-language to
  check and enforce these invariants.  Our main contribution is the
  illustration of the utility of type equality in typed functional
  meta-programming. In particular, we encode and capture judgments
  about many important language features using type equality. Finally,
  we show how type equality is incorporated as a feature of the type
  system of a practical functional meta-programming language.
  
  The core of this thesis is divided into three parts.
  
  First, we design a meta-programming language with dependent types.
  We use dependent types to ensure that well-typed meta-programs
  manipulate only well-typed object-language programs.  Using this
  meta-language, we then construct highly efficient and safe
  interpreters for a strongly typed object language. We also prove the
  type safety of the meta-language.
  
  Second, we demonstrate how the full power of dependent types is not
  necessary to encode typing properties of object-languages.  We
  explore a meta-language consisting of the programming language
  Haskell and a set of techniques for encoding type equality.  In this
  setting we are able to carry out essentially the same
  meta-programming examples. We also expand the range of
  object-language features in our examples (e.g., pattern matching).
  
  Third, we design a meta-language (called Omega) with built-in
  equality proofs. This language is a significant improvement for
  meta-programming over Haskell: Omega's type system automatically
  manipulates proofs of type equalities in meta-programs.  We further
  demonstrate our encoding and meta-programming techniques by
  providing representations and interpreters for object-languages with
  explicit substitutions and modal type systems.
},
  author = {Pasalic, Emir},
  date-added = {2004-12-09 15:41:18 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  school = {Oregon Health and Sciences University, The OGI School of Science and Engineering},
  title = {The Role of Type Equality in Meta-Programming},
  url = {http://emirpasalichome.appspot.com/p2/papers/thesis.pdf},
  year = {2004},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/thesis.pdf}
}
@article{SP04,
  abstract = {In this paper, we describe two techniques for the efficient, modularized implementation of
a large class of algorithms. We illustrate these techniques using several examples, including
efficient generic unification algorithms that use reference cells to encode substitutions, and
highly modular language implementations.
We chose these examples to illustrate the following important techniques that we believe
many functional programmers would find useful. First, defining recursive data types by
splitting them into two levels: a structure defining level, and a recursive knot-tying level.
Second, the use of rank-2 polymorphism inside Haskell's record types to implement a kind
of type-parameterized modules. Finally, we explore techniques that allow us to combine
already existing recursive Haskell data-types with the highly modular style of programming
proposed here.
},
  author = {Sheard, Tim and Pasalic, Emir},
  date-added = {2004-12-09 15:44:29 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  journal = {Journal of Functional Programming},
  month = {September},
  number = {5},
  pages = {547--587},
  rating = {1},
  title = {Two-Level Types and Parameterized Modules},
  url = {http://emirpasalichome.appspot.com/p2/papers/JfpPearl.pdf},
  volume = {14},
  year = {2004},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/JfpPearl.pdf}
}
@unpublished{PST:2000,
  abstract = {Writing (meta-)programs that manipulate other (object-)
  programs poses significant technical problems when the object-language
  itself has a notion of binders and variable occurrences.  Higher-order
  abstract syntax is a representation of object programs that has recently
  been the focus of several studies. This paper points out a number of
  limitations of using higher order syntax	in a functional context, and
  argues that Dali, a language based on a simple and elegant proposal
  made by Dale Miller ten years ago can provide superior support for
  manipulating such object-languages.  Miller's original proposal,
  however, did not provide any formal treatment.  To fill this gap, we
  present both a big-step and a reduction semantics for Dali, and
  summarize the results of our extensive study of the semantics, including
  the rather involved proof of the soundness of the reduction semantics
  with respect to the big-step semantics. Because our formal development
  is carried out for the untyped version of the language, we   hope it
  will serve as a solid basis for investigating type system(s) for
  Dali.},
  author = {Pasalic, Emir and Sheard, Tim and Taha, Walid},
  date-added = {2004-12-09 15:46:54 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  note = {Unpublished.},
  title = {Dali: An Untyped, CBV Functional Language Supporting First-Order Datatypes with Binders},
  url = {http://emirpasalichome.appspot.com/p2/papers/dali.pdf},
  year = {2000},
  bdsk-url-1 = {http://emirpasalichome.appspot.com/p2/papers/dali.pdf}
}
@unpublished{PT03,
  author = {Pasalic, Emir and Sheard, Tim},
  date-added = {2004-12-09 15:48:23 -0600},
  date-modified = {2007-02-01 13:51:12 -0600},
  note = {Unpublished.},
  title = {Implementing Pattern-based Binding in typed Object languages},
  year = {2003}
}