Systems-Level Design Group

General

Hansen and MacNamee -  Efficient Reading of Papers in Science and Technology -  Reading papers to try and learn the literature in any area of research can be daunting. This nice 2-page handout discusses some excellent pointers on how to efficiently read technical papers.

Composable Interpreters

Interpreters in our laboratory are currently written using a technique developed by the semantics community called composable, monadic interpreter construction. They involve writing and composing AST elements, writing a semantic algebra for each AST element, finding the least fixed point, and using a catamorphism for interpretation.

Graham Hutton -  Fold and Unfold for Program Semantics -  This tarball contains both the Hutton paper and a companion report documenting interpreters using the folding techinques from the paper.

Luc Duponcheel -  Using catamorphisms, subtypes and monad transformers for writing modular functional interpreters -  This tarball contains both the Duponcheel paper and a companion report documenting interpreters using the composition techniques from the paper.

Monads

Moggi introduced the concept of a monad to represent computations. Commonly used in pure-functional languages to represent various styles of computation with and without side effects, we believe monads will form the basis of modeling and evaluating Rosetta facets.

Phillip Wadler -  How to declare an imperative -  Examines the motivation behind using monads to model side effects in a pure functional programming language.

Phillip Wadler -  Monads for Functional Programming -  Provides more background on Monads.

Phillip Wadler -  The Essence of Functional Programming -  Includes several examples of using monads.

Liang, Hudak, and Jones -  Monad Transformers and Modular Interpreters -  Introduces monad transformers for combining monads which support the creation of modular interpreters.

Mark Jones -  Composing Monads -  Describes some rules and theory behind the composition of different monad transformers. The parsers we write in our laboratory make heavy use of techniques from this paper.

Ralf Hinze -  Deriving Backtracking Monad Transformers -  Demonstrates how to derive programs from their specifications. The paper derives a monad for supporting backtracking as seen in logic programming languages.

Hughes -  Generalising Monads to Arrows -  Describes a more abstract version of a monad called an arrow. The use of an arrows allows for more aggressive static analysis of monadic computations.

Category Theory and Semantics

Category theory provides an exceptionally general mechanism for describing the properties of objects without referencing their structure. It also provides a semantics for object composition and has been used extensively in program synthesis and semantics.

C. Barry Jay -  An Introduction to Categories in Computing -  An excellent introduction to category theory concepts

Benjamin Pierce -  Basic Category Theory for Computer Scientists -  Abook describing category theoretic concepts important specifically for computer science.

Andrea Asperti and Giuseppe Longo -  Categories, Types and Structures -  A general text on category theory divided into theoretical and application sections.

Lambert Meertens -  Category Theory for Program Construction by Calculation -  A wonderful introduction to category theoretic techniques for program synthesis. This work is quite approachable even if you have little specific category theory background.

Generic and Polytypic Programming

Many algebraic types are similar in the having a common shape, dictated by the type's recursive definition. These papers try to generalize functions over types with a common shape.

Meijer, et al -  Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire -  Introduces common recursion schemes in functional programming and provides methods for using and reasoning about these recursion schemes.

Meijer and Hutton -  Bananas in Space: Extending Fold and Unfold to Exponential Types -  Generalizes the above paper, which is concerned primarily with list types, to general algebraic types.

Duponcheel -  Writing Interpreters using Catamorphisms, Subtypes, and Monad Transformers -  Combines the use of monad transformers with generic programming techniques to build interpreters.

Gayo -  Reusable Monadic Semantics of Logic Programs with Arithmetic Predicates -  Provides an example of using the methods from the above paper to extend a simple prolog-like logic programming language with arithmetic operations.

Jansson and Jeuring -  Polytypic Unification -  Gives a generic unification algorithm, such as that used by Prolog. It then uses generic programming techniques to make the algorithm work for any term type, automatically.

Domain Specific Extension Languages

DSELs are attempts to extend languages to provide capabilities specific to a particular domain. Rosetta domains are in effect semantic DSELs. Understanding DSELs and their implementation will help in understanding the implementation of evaluators for individual Rosetta domains.

Flow Analysis and Abstract Interpretation

Flow analysis and abstract interpretation are static techniques for evaluating properties of code fragments. (Coming Soon)

 -  Bandera - 

Patrick Cousot -  Abstract Interpretation -  Computing Surveys overview of abstract interpretation techniques.

David Schmidt and Bernhard Steffen -  Program Analysis as Model Checking of Abstract Interpretations  -  Static analysis techniques that combine model checking and abstract interpretation.

Flemming Nielson, Hanne R. Nielson and Chris Hankin -  Principles of Program Analysis -  An excellent overview of several static analysis techniques. We use this text for our graduate static analysis course.

Proof Carrying Code

Proof-carrying code is a technique used to reduce the need for source authentication when executing mobile code.

Greg Morrisett, et. al. -  From System F to Typed Assembly Language -  Overview paper on typed assembly language techniques. An alternative to this paper is the chapter by Morrisett in Pierce's advanced types text.

George Necula -  Proof-Carrying Code -  One of the original descriptions of proof-carrying code. An alternative to this paper is the chapter by Necula in Pierce's advanced types text.

Software Synthesis

Software synthesis includes techniques for moving from high level specifications to executable code.

Douglas Smith -  KIDS: A Semiautomatic Program Development System -  Classic paper on category theoretic techniques for synthesizing programs from axiomatic specifications.

Manna and Waldinger -  Fundamentals of Deductive Program Synthesis -  Classic paper on use of tableau theorem proving to synthesize programs.

 -  Source Transformation - 

Programming Language Links

ML - A call-by-value, strict, functional language somewhat like Haskell in appearance, but very different in implementation. The ML module system and type inference systems are quite interesting. ML and it's derivative OCAML have attracted significant recent interest.

OCAML - An object-oriented derivative of ML. Growing in popularity in several areas such as network programming. Compiles to an interesting virtual machine that is an alternative to the Java virtual machine. Definitely worth a look.

Haskell - A lazy, non-strict functional language. Interesting class system in contrast to the C++/Java style. We do most of our development in Haskell.

Haskore - A domain specific language built on Haskell for functional representation of music. We may play around with Haskore in one of our projects.

Scheme - A functional language in the Lisp family. Highly consistent and relatively small, Scheme is a favorite among language researchers. The PLT folks have done a wonderful job of supporting and promoting Scheme in teaching as well as research.

Common Lisp - An alternate implementation of Lisp that shares many concepts with Scheme. While Scheme is intended to be small and highly consistent, Common Lisp has an expansive feature set. Of particular interest is the excellent object-oriented extension called CLOS (Common Lisp Object System).

Erlang - A functional / parallel programming language. Erlang computations are purely functional and embedded in a parallel programming language based on the pi calculus.

SmallTalk - Largely viewed as the first fully object oriented language, SmallTalk was developed in the 1970s and still enjoys substantial usage. The terms "message" and "method" commonly used in describing object oriented systems emerged from the SmallTalk language. While languages like Common Lisp, C++ and Java use generic functions to implement object-oriented features, SmallTalk uses the classic message-method approach. Loosely defined, a message is sent to an object requesting an action be performed. The object responds with a method associated with the message. Note that this is not parallel programming or message passing in the distributed programming sense.

Prolog - A widely used logic programming language. Instead of describing how a computation is performed, properties of the solution are defined. The prolog interpreter takes the problem description and determines how to satisfy it. Prolog is particularly popular in the European artificial intelligence community.

Perl - Perl is among the most popular scripting languages currently in use. With bindings to many libraries, a powerful pattern matching capability, and many other scripting features, you will definitely find Perl useful for scripting, CGI writing and other day-to-day tasks. Perl will be installed by default in virtually any Linux environment. Take a look at the FAQ and info to find out more.

Python - Rapidly approaching perl, python is another example of a scripting language useful for day-to-day computing tasks. Although python shares features with perl, it is much better suited for developing larger applications. It's dictionary capability is particularly useful and interesting. Python will be installed by default on any Linux environment. Take a look at the FAQ and info to find out more.

Ruby - An object-oriented scripting language.

Esterel - A synchronous language used for describing control systems and hardware systems. Synchronous refers to the concept of a clock and triggering execution on changes in signals.

SETL - A language whose basic data structures and operations center on using sets.

Oz and Mozart -

CafeOBJ - A formal language environment implementing the OBJ formal specification language. The language implements algebraic theories and insitutions providing both formal analysis capabilities and executability. CafeOBJ differs from most langauges in that it is highly formal with a clean mathematical syntax.

VHDL - A special purpose simulation language for digital hardware systems. VHDL is much like Ada in style, but much different in implementation. VHDL centers on entities that represent chips or processes. A collection of interconnected entities is used to describe a system. All entities execute in parallel and respond to changes in signals to control execution. While traditional languages traditionally check the value of a variable, VHDL signals can be monitored for changes in value using wait statements and sensitivity lists. Electrical Engineers and Computer Engineers at KU learn VHDL in EECS 443.

Verilog - A special purpose simulation langauge for digital hardware systems. Verilog was originally developed by Cadence as a proprietary modeling language. The emergence of VHDL in the 1980's brought Verilog into the public domain. Where VHDL tends to be Ada-like, Verilog tends to be more C-like in philosophy.

SystemVerilog - An extension of Verilog into "system-level" design. Subsumes Verilog.

SystemC - A C++ based open source language and simulation kernel for modeling and implementing electronic systems. SystemC is an excellent example of a domain-specific embedded language for hardware modeling.

Lava - A domain specific embedded language extending Haskell for hardware system modeling.

Rosetta - A specification language for heterogeneous systems developed by researchers at The University of Kansas working through ITTC. Rosetta is being standardized by Accellera for use modeling and simulating heterogeneous hardware and software systems. Rosetta is loosely based on concepts from Haskell, VHDL and many other languages.