IU Programming Languages Group

Here are the (self-selected) members of our group (alphabetically by first name). If you'd like to be listed as a member, please mail K.D.P.Ross, including your name (and how you'd like it spelt), your research interests, e-mail, web-site, etc., and a picture of yourself.

Amr Sabry

Amr likes quantum programming, TOTW, and being harassed by Kyle and Roshan. Here is his web page.

Aziz Ghuloum

Aziz does things with compilers, especially Scheme compilers. He loves macros and hates types.

Dan Friedman

likes Scheme and parens. He doesn't think that "cons" should evaluate its arguments. He likes to have fun with logic programming (and monads!). Dan's so cool that he has a page on Wikipedia.

Joe Near

does cool things with theorem provers.

K.D.P.Ross

kyle (at) osl (dot) iu (dot) edu

I am a Ph.D. student at IU. Previously, I've studied at Rensselaer and Chalmers.

I'm interested in functional programming, pure type systems, dependent types, semantics, intuitionism, and evolving types. To explore my ideas, I develop Braque, an experimental evolving-type-enabled language. My academic web site (which has some more information about these interests, projects that I tinker with, and, excitingly enough, a constructive proof of a bound on my Erdös number) can be found here.

In my non-work time, I enjoy photography, travel, cooking, wine, watching unusual films, and sitting in the sun.

I maintain this page, so please contact me with any questions about it or about the PL Group; I'll either answer them or do my best to forward it to the right person.

R. Kent Dybvig

Kent loves Scheme so much that he wrote his own Scheme compiler. Like Dan, he has a page on Wikipedia.

Michael D. Adams

Michael likes monads and matrices.

Ron Garcia

Ron is very smart. He does all sorts of cool things including metaprogramming stuff. He has cool hair.

Roshan P. James

Rosh has no head because he thinks that women prefer him this way. He has fancy lenses and a camera that works. He loves yield the magnificent and hates Linux.

Will Byrd

Will is enamoured with logic programming and nominal logic programming. He enjoys running his programs backwards (and sometimes forwards).

We give talks about our work and interesting PL-related topics, usually on Friday afternoons. Here is a list of our talks, some of which have slides, code, etc. that you can download.

2008-01-18–"Nominal Techniques in the Theorem Prover Isabelle –or– How Not to be Intimidated by the Variable Convention" (Christian Urban, TU Munich)
2008-02-01–"Software Transactional Memory: Going faster!" (Roshan James)
2008-02-08–"(Toward) A Theory of Hygienic Macros" (Dave Herman, Northeastern)
2008-02-15, 2008-02-29, 2008-04-04–multi-part Coq & locally-nameless-variables tutorial (Ron Garcia)
2008-02-22–"Ruby: Powerful, but Slow" (Andy Keep)
2008-03-07–"Scrapping Scrap your Nameplate" (Michael D. Adams)
2008-03-21–"Asynchronous Concurrent Programming in CCR and its application on the Web-service work-flow engine" (Wei Lu)
2008-04-11–"Modelling a Metaprogramming Language" (Ron Garcia)
2008-04-18–"AlphaTAP: a declarative theorem prover" (Joe Near)
AlphaTAP is available here.

We have a reading group where we discuss interesting topics. We're focusing on binding / names now.

2008-02-12–"Practical Foundations for Programming Languages" (excerpts)(R.Harper)
2008-03-11–"A Self-Hosting Evaluator using HOAS" (E.Barzilay)
2008-04-08–"Nominal Logic and Abstract Syntax" (J.Cheney)
2008-04-08–"Higher-Order Abstract Syntax: Setting the Record Straight" (K.Crary and R.Harper)
2008-04-22–"A Metalanguage for Structural Operational Semantics" (M.R.Lakin and A.M.Pitts)

Here are some links where you can find out more about our favourite / interesting programming languages!

Agda
Agda is a dependently typed programming language with good support for programming with inductively defined families of types.
Coq
Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: to define functions or predicates, to state mathematical theorems and software specifications, to develop interactively formal proofs of these theorems, to check these proofs by a relatively small certification "kernel".
Haskell
Haskell is an advanced purely functional programming language. The product of more than twenty years of cutting edge research, it allows rapid development of robust, concise, correct software. With strong support for integration with other languages, built-in concurrency, debuggers, profilers, rich libraries and an active community, Haskell makes it easier to produce flexible, maintainable high-quality software.
MiniKanren
Kanren is a declarative logic programming system with first-class relations, embedded in a pure functional subset of Scheme. The system has a set-theoretical semantics, true unions, fair scheduling, first-class relations, lexically-scoped logical variables, depth-first and iterative deepening strategies. The system achieves high performance and expressivity without cuts.
OCaml
Caml is a general-purpose programming language, designed with program safety and reliability in mind. It is very expressive, yet easy to learn and use. Caml supports functional, imperative, and object-oriented programming styles. It has been developed and distributed by INRIA, France's national research institute for computer science, since 1985.
Scheme
Scheme is a multi-paradigm programming language. It is one of the two main dialects of Lisp and supports a number of programming paradigms but is best known for its support of functional programming.
- Chez Scheme
- Ikarus
Standard ML
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.
- SMLNJ