Tim Sheard

Full Professor,

Portland State University

Computer Science Department

Ph.D. University of Massachusetts at Amherst, 1985

office FAB 120-04, phone: 503-725-2410


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).

"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 Curry-Howard 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.

Since 2004, my students and I have written many papers on that and related topics.

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, Chuan-Kai Lin, has writen and defended a thesis Practical Type Inference for the GADT Type System. Defended June 1st, 2010.

My student, Nathan Mishra-Linger, 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 Meta-Programming. It explains the connection between Logic and Generalized Algebraic Data Types.

My student, Walid Taha, has writen and defended a thesis Multi-Stage 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). Co-located with OOPSLA'04, October 24-28, 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 meta-programming systems. I have written a taxonomy of meta-programming systems, and has built the meta-programming language MetaML, and designed the Template Haskell extension to the Glasgow Haskell compiler. I am also interested in applying meta-programming 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.

This material is based upon work supported by the National Science Foundation under Grants No. 0910500 and CCF-0541447 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.