New October 10, 2014. I have finally finished my academic genealogy. Take a look and
see who had a hand in shaping my world.
New april 29, 2011. There is new release of the Omega interpreter.
Visit the download page to see how you can install a version
for your self. This page has also been translated into Swedish.
New May 11, 2007.
I gave a lecture about the Lambda Calculus as a guest lecturer for
Jim Hook's "Theory of Computation" class. To illustrate my talk
I wrote a little Haskell program I call the Lambda Caculator. It was so much
fun, the students wanted to try it out. Read about it and download it here.
This page has also been translated into Swedish.
Courses I am teaching (or have taught).
 In Fall 2015 I am teaching CS457/557 Functional Languages.
 In winter 2015 I taught CS558 Programming Languages.
 In winter 2015 I taught CS457/557 Functional Languages.
 In Fall 2014 I taught Mathematical Logic and Programming Languages.
 In spring 2014 I taught Advanced Functional Programming.
 In winter 2014 I taught CS558 Programming Languages.
 In Fall 2013 I taught CS311, Computational Structures.
 In Spring 2013 I taught CS581 Theory of Computation.
 In Winter 2013 I taught Functional Languages CS457/557.
 In Winter 2013 I did not teach Mathematical Logic via Foundational Algorithms. See here for information.
 In Fall 2012 I taught CS311, Computational Structures.
 In Spring 2011 I taught CS311, Computational Structures.
 In Winter 201 I taught CS 457557, Functional Languages.
 Winter 2011 I cotaught Logic via Foundational Algorithms with Jim Hook.
 Fall 2010 I cotaught Scholarship Skills with Andre Black.
 In spring 2010 I taught a
seminar
on dependently typed programming
using Omega.
 In Winter 2010 I taught CS 457557, Functional Languages.
 In Fall 2009 I taught Cs 163, Data Structures.
 In the spring 2009, winter 2009, and fall 2008 quarters, I taught
Cyber Millenium, a Freshman Inquiry Course.
The Haskell programming resource page
Guest Lectures for Leslie Batchelder's section.
 In spring 2009, I am teaching Functional Programming with Mark Jones.
 In 2007 (fall,winter, and spring quarters), I taught
Design & Society, a Freshman Inquiry Course.
 In the spring quarter 2007, I taught
Programming Languages and Compilers part II. and
Advanced Programming.
 In the winter quarter 2007, I taught
Programming Languages and Compilers part I.
 In the spring quarter 2006, I taught
Programming Languages and Compilers part II. and
Advanced Programming.
 In the winter quarter 2006, I taught
Programming Languages and Compilers part I. and
Scholarship Skills.
 In the spring quarter 2005, I taught
Applied Algorithms.
 In the winter quarter 2005, I taught
Fundamentals of Staged Computation.
 In the fall quarter 2004, I taught
Introduction to Functional Programming.
 In 2003, I taught
Advanced Functional Programming at OGI, here are the course notes.
"Generalized Algebraic Data
Structures" have become a a hot new topic. They have recently been added to the GHC compiler.
They support the construction,
maintenance, and propagation of semantic properties of
programs using powerful old ideas about types (the
CurryHoward Isomorphism) in surprisingly easy to understand
new ways. The language Omega was designed and implemented to demonstrate their utility.
Here a a few talks I gave that explains how they work.
 September 2004. The first is a talk in which I explained them at the
Haskell Workshop in Snow Bird Utah.
 October 2004. The second is a set of notes from a seminar talk at Portland State University about
similar material, but aimed at an audience with less functional
programming knowledge.
 November 2004. The third is my OOPSLA Onward Session Talk:
Languages of the Future
This talk requires even less functional programming background and
is probably the most accessible set of slides. The companion
paper
contains an even more detailed explanation
Since 2004, my students and I have written many papers on that and related topics.

Erasure and Polymorphism in Pure Type Systems.
(bib)
Explains how an erasure semantics for pure type systems (a generalization of many dependently
types languages) leads a to new notion of polymorphism. Key ideas from Nathan Lingers Thesis.
Fossacs 2008. LNCS 4962.

Programming In Omega.
(bib)
Notes from the 2nd Central European
Functional Programming School, June 2330, 2007. A careful
explanantion of many of Omega's more recent features, plus
a whole new set of examples, including trees and paths with shape,
AVL trees, and a subject reduction theorem for the lambda calculus. LNCS 5161

Generic Programming In Omega,
(bib)
Spring school on Generic Programming, April 2006. LNCS 4719.

Types and Hardware Description Languages
(bib)
The Hardware design and Functional Languages workshop,
March 2007. A satelite event of the ETAPS 2007.

TypeLevel Computation Using Narrowing in Omega.
(bib)
Presented at PLPV'06, Seattle, WA. August 2006.
Electronic Notes in Theoretical Computer Science 1643
Volume 174, Issue 7.

MetaProgramming with Typed ObjectLanguage Representations.
(bib)
Presented at GPCE, Vacouver B.C. Oct 2004. Emir Pasalic and Nathan Linger

Metaprogramming with Builtin Type Equality.
(bib)
Presented at Logical Frameworks and MetaLanguages
workshop, Cork Ireland, July 2004.

A new REVISED VERSION of Languages of the Future.
(bib)
A forward looking paper presented at the Onward Track of the
2004 OOPLSA conference. The full
paper was reprinted in the December, 2004, SIGPLAN Notices.

A draft of Programming with Static Invariants in Omega.

A draft of GADTs + Extensible Kinds = Dependent Programming.
(bib)

The third revision of Playing with Types.
(bib)
An exploration
of using Omega as a metalanguage in the design of type systems for
new objectlanguages. Introduces a new type system for MetaML as an Omega
program.

Haskell 2005 Workshop Putting Curry Howard to Work.
(bib)
How to put the CurryHoward isomorphism to work to state
interesting properties of real programs. Introduces the Omega's
static propositions.

A paper entitled
Another Look at Hardware Design Languages.
(bib)
that discusses how ideas in Omega could be used to
build better hardware description languages.
Some Omega programs we have written to illustrate the use of Omega. (Lots more examples in the papers above.)
Many other people explored similar ideas in the development of GADTs.
Here is a somewhat outdated set of links.
Student Disserations.
My student, ChuanKai Lin, has writen and defended
a thesis
Practical Type Inference for the GADT Type System.
Defended June 1st, 2010.
My student, Nathan MishraLinger, has written and defended a thesis on
Irrelevance, Polymorhism, and Erasure in Type Theory.
It explains how an erasure semantics for pure type systems leads new notions
of computational irrelevance and polymorphism. He succesfully defned his thesis
Nov. 7, 2008.
My student, Emir Pasalic, has written and defended a thesis on
The Role of Type Equality in MetaProgramming.
It explains the connection between Logic and Generalized Algebraic
Data Types.
My student, Walid Taha, has writen and defended
a thesis
MultiStage Programming: Its Theory and Applications.
It describes the theory and practice of staged languages
such as MetaML.
Research Interests
I was the General Chair of the Generative Programming and Component Engineering
Conference (GPCE'04). Colocated with OOPSLA'04, October 2428, 2004.
Vancouver, British Columbia, Canada.
I organized the 5th ICFP programming contest (2002)
and the 11th ICFP programming contest (2008).
I am the creator of MetaML See the
homepage
for download and installation instructions.
I am actively pursuing research in the design, implementation, and application of
dependently typed programming languages. I view Omega as a first attempt.
I am working with Aaron Stump
and Stephanie Weirich to combine
some of ideas and experience. See http://www.trellys.org/
I am actively pursuing research in the design, implementation, and application of
metaprogramming systems. I have written a
taxonomy of metaprogramming systems, and has built the
metaprogramming language
MetaML,
and designed the Template Haskell extension to the Glasgow Haskell compiler.
I am also interested in applying
metaprogramming systems to
domain specific languages.
To see what I've thought about in the not
too distant past, read a few of the NSF proposals I submitted a few years ago.
Combining Programming Languages and Logical Reasoning Systems
and
Evolving Domain Specific Languages
.
Older papers I have written.

Metaprogramming with Builtin Type Equality.
Logical Frameworks and MetaLanguages, 2004.

Languages of the Future.
A forward looking paper thjat will be presented at the Onward Track of the
2004 OOPLSA conference.

BindingTime Analysis for MetaML via Type Inference and Constraint Solving.
TACAS'04, Barcelona Spain, March 2004.

A Pure Language with Default Strict Evaluation Order and Explicit Laziness.
This paper was submitted to the 2003 Haskell Workshop. It didn't appear
in the proceedings, but was discussed in one of the 10 minute new results sessions.

TwoLevel Types and Parameterized Modules. With
Emir Pasalic. Expanded
version of Generic Unification via TwoLevel Types and Parameterized Modules,
with new examples. JFP 14 (5):547587, Sept. 2004

Tagless Staged Interpreters for Typed Languages.
With Emir Pasalic and Walid Taha. ICFP'02.

Template Metaprogramming for Haskell.
With Simon Peyton Jones. Haskell Workshop, Pittsburgh, October 2002.

SearchBased Binding Time Analysis using TypeDirected Pruning.
With Nathan Linger. Pepm'02, Aizu Japan.

Staging Algebraic Datatypes. With Iavor Diatchki.

Accomplishments and Research Challenges in MetaProgramming
. Invited Talk to SAIG 2001.
Also available online from LNCS, Volume 2196.

Generic Unification via TwoLevel Types and
Parameterized Modules. Conference record of ICFP'01
 Dynamically Adaptable Software with
Metacomputations in a Staged Language . With Bill Harrison. SAIG 2001. LNCS 2196

Fine Control of Demand in Haskell.
With William Harrison and Richard Kieburtz. MPC'02

DSL Implementation Using Staging and Monads.
Usenix
DSL '99

Using MetaML: A staged Programming Language.
Lecture notes of the Summer School on Advanced Functional Programming. September 1998. Braga, Portugal
(LNCS 1129)
 MultiStage Programming:
Axiomatization and Type Safety ICALP'98 (postscript)
 Dynamic Typing through Staged Type Inference. POPL '98 (postscript)
 Multistage Programming with Explicit Annotations PEPM '97 (postscript)
 A TypeDirected, Online Partial Evaluator for a Polymorphic Language PEPM '97 (postscript)
 Revisiting Catamorhpisms over Datatypes with Embedded Functions POPL'96 (postscript)
 Warm Fusion: Deriving BuildCata's from Recursive Definitions FPCA '95 (postscript)
 Facets of MultiStage Computation in Software Architectures with Walid Taha (gziped postscript)
 A Fold for all Seasons FPCA '93 (postscript)
 The MetaML Manual
This material is based upon work supported by the National Science
Foundation under Grants No. 0910500 and CCF0541447 and 0613969.
Any opinions, findings, and conclusions or recommendations
expressed in this material are those of the author(s) and do not
necessarily reflect the views of the National Science Foundation.