Dependently Typed Programming

NII Shonan Meeting:

@ Shonan Village Center, Sep. 14-17, 2011(Check-in: the night before)

NII Shonan Meeting Report (ISSN 2186-7437):No. 2011-3

Organizers:

  • Shin-Cheng Mu (Academia Sinica, Taiwan)
  • Conor McBride (University of Strathclyde, UK)
  • Stephanie Weirich (University of Pennsylvania, USA)

 

Overview

A thriving trend in computing science is to seek formal, reliable means of ensuring that programs possess crucial correctness properties.

One path towards this goal is the design of high-level programming languages which enforces that program, by their very own structure, behave correctly. In the past decade, the use of type systems to guarantee that data and program components be used in appropriate ways has enjoyed wide success and is still a main focus both from researchers and developers.

With more expressive type systems, the programmer is allowed to specify more fine-grained properties the program is supposed to hold. Dependent type systems, allowing types to refer to (hence depend on) data, are particularly powerful since they reflect the reality that what defines “appropriate” program behaviours is often dynamic. With the type system, programmers are free to communicate the design of software to computers and negotiate their place in the spectrum of precision from basic memory safety to total correctness.

Dependent types have their origin in the constructive foundations of mathematics, and have played an import role in theorem provers. Advanced proof assistants, such as Coq, has been used to formalise mathematics (e.g. the proof of the four colour theorem) and verify compilers. Only recently have they begun to be integrated into programming languages. The results so far have turned out to be fruitful. A number of dependently typed programming language and systems have been proposed, including Cayenne, DML, Epigram, Ωmega, ATS, Agda, Guru, etc, showing a maturity beyond the proof-of-concept stage. Papers on dependent types submitted to and published in major conferences have significantly increased in number. Some more “mainstream” functional programming languages, such as Haskell, also start to adopt features such as GADT and type family that are strongly influenced by dependent types.

Dependently typed programming, however, is yet to be considered a practical tool and an efficient device to ensure program correctness and to reduce development costs. Many issues remain to be resolved, including but not limited to:

_ design of a small but expressive core language on which to built up a verifiable metatheory;

_ metaprogramming, reflectivity, and the possibility of representing dependently typed terms in a dependently typed language;

_ representing variable-binding and supporting both structural inspection and functional usage;

_ interpreting representations to automate problem solving;

_ separating and redesigning a language of “proof” as distinct from a language for “programming”;

_ integrating extensional reasoning about functions with computation in dependent type systems, while at the same time concealing the internal structure of proofs;

_ modelling interaction and communication in distributed, concurrent systems using dependent types.

This workshop aims to provide a venue for people actively working in this field so that these issues could be discussed.

 

8 comments

  1. This was great fun – productive meeting, splendid facilities, beautiful location. I recommend the walk up Mt Ogusuyama for the view. It’s about 3km each way, well surfaced and sign-posted – but it’s quite steep.

  2. Participant

    Access to Shonan village is exalted.

  3. Participant

    Good! Interesting meeting. Longer breaks would have been nice, but I enjoyed the non-rushed talks with plenty of discussion.

  4. Participant

    I would have liked “onsen” culture no part of the meeting.

  5. Participant

    I very much appreciate the effort to reproduce “Dagstuhl” in Japan. But I think some important elements are missing:library is an important part of Dagstuhl; workshop structure is much more open, fewer talks.

  6. Participant

    7 day meeting allows time for ideas.

  7. I relished scanning this document, I’d been only irritation to recognise can you industry highlighted articles or blog posts? We’re consistently on the lookout for anyone to produce trades along with along with merely believed I’d personally consult.

  8. Greetings, I am writing from the Gold Coast, Australia. Thanks for the thoughtful content. It helped me a lot with my school computing assignment 🙂