[1] Molham Aref, Benny Kimelfeld, Emir Pasalic, and Nikolaos Vasiloglou. Extending datalog with analytics in logicblox. In Andrea Cali and Maria-Esther Vidal, editors, Proceedings of the 9th Alberto Mendelzon International Workshop on Foundations of Data Management, Lima, Peru, May 6 - 8, 2015., volume 1378. CEUR-WS.org, 2015. [ bib | .pdf ]
[2] Molham Aref, Balder ten Cate, Todd J. Green, Benny Kimelfeld, Dan Olteanu, Emir Pasalic, Todd L. Veldhuizen, and Geoffrey Washburn. Design and implementation of the logicblox system. In Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data, SIGMOD '15, pages 1371--1382, New York, NY, USA, 2015. ACM. [ bib | DOI | http ]
Keywords: datalog, incremental maintenance, leapfrog triejoin, live programming, logicblox, logiql, predictive analytics, transaction repair
[3] David Zook, Emir Pasalic, and Beata Sarna-Starosta. Typed Datalog, pages 168--182. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. [ bib | DOI | http ]
[4] Beata Sarna-Sarosta, David Zook, Emir Pasalic, and Molham Aref. Relating constraint handling rules to datalog. In Fifth Workshop on Constraint Handling Rules, July 2008. [ bib ]
[5] Tim Sheard and Emir Pasalic. Meta-programming with built-in type equality (journal version). Electron. Notes Theor. Comput. Sci., 199:49--65, 2008. [ bib | DOI ]
[6] Jason Eckhardt, Roumen Kaiabachev, Emir Pasalic, Kedar Swadi, and Walid Taha. Implicitly heterogeneous multi-stage programming. New Generation Computing, 25(3):305--336, 2007. [ bib | DOI | http ]
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.

[7] Seth Fogarty, Emir Pasalic, Jeremy Siek, and Walid Taha. Concoqtion: Indexed types now! In ACM SIGPLAN 2007 Workshop on Partial Evaluation and Program Manipulation (PEPM '07), 2007. [ bib | .pdf ]
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.

[8] Emir Pasalic, Jeremy Siek, and Walid Taha. Concoqtion: Mixing indexed types and hindley-milner type inference. Unpublished., 2006. [ bib | .pdf ]
[9] Kedar Swadi, Walid Taha, Oleg Kiselyov, and Emir Pasalic. A monadic approach for avoiding code duplication when staging memoized functions. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '06). ACM Press, January 2006. [ bib | .pdf ]
[10] Jason Eckhardt, Roumen Kaiabachev, Emir Pasalic, Kedar Swadi, and Walid Taha. Implicitly heterogeneous multi-stage programming. In Proceedings of the 4th ACM International Conference on Generative Programming and Component Engineering (GPCE'05), volume 3676 of Lecture Notes In Computer Science. Springer-Verlag, September 2005. [ bib | .pdf ]
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.

[11] Emir Pasalic and R. Nathan Linger. Meta-programming with typed object-language representations. In Gabor Karsai and Eelco Visser, editors, Generative Programming and Component Engineering: Third International Conference. Lecture Notes in Computer Science, Springer-Verlag, October 2004. [ bib | .pdf ]
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.

[12] Tim Sheard and Emir Pasalic. Two-level types and parameterized modules. Journal of Functional Programming, 14(5):547--587, September 2004. [ bib | .pdf ]
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.

[13] Tim Sheard and Emir Pasalic. Meta-programming with built-in type equality. In Logical Frameworks and Meta-Languages workshop. Proceedings., 2004. [ bib | .pdf ]
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.

[14] Emir Pasalic. The Role of Type Equality in Meta-Programming. PhD thesis, Oregon Health and Sciences University, The OGI School of Science and Engineering, 2004. [ bib | .pdf ]
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.

[15] Emir Pasalic and Tim Sheard. Implementing pattern-based binding in typed object languages. Unpublished., 2003. [ bib ]
[16] Emir Pasalic, Tim Sheard, and Walid Taha. Tagless staged interpreters for typed languages. In The International Conference on Functional Programming (ICFP '02). ACM, ACM Press, October 2002. [ bib | .pdf ]
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.

[17] Andrew Moran, James Teisher, Andrew Gill, Emir Pasalic, and J. Veneruso. Automated translation of legacy code for ATE. In International Test Conference 2001 (ITC '01), pages 148-- 156. IEEE, October 2001. [ bib | .pdf ]
[18] Emir Pasalic, Tim Sheard, and Walid Taha. Dali: An untyped, cbv functional language supporting first-order datatypes with binders. Unpublished., 2000. [ bib | .pdf ]
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.

[19] Tim Sheard, Zine-el-Abidine Benaissa, and Emir Pasalic. Dsl implementation using staging and monads. In Second Conference on Domain-Specific Languages (DSL'99), pages 81--94, New York, NY, USA, October 1999. USENIX, ACM Press. [ bib | .pdf ]
[20] Judith Bayard Cushing, Justin Laird, Emir Pasalic, Elizabeth Kutter, Tim Hunkapiller, Frank Zucker, and David P. Yee. Beyond interoperability - tracking and managing the results of computational applications. In Ninth International Conference on Scientific and Statistical Database Management. IEEE Computer Society Press, 1997. [ bib ]