The first Middle-Earth Programming Languages Seminar (MEPLS1) will be held on Saturday, September 6, 2008 in the Mabee Business Building (MBB) at Abilene Christian University.
MEPLS was formed to encourage collaboration between researchers, students and praticitioners interested in software correctness, including areas such as programming languages, theorem proving, and formal methods. Our goal is to increase awareness of each other's work, and to encourage interaction and collaboration. We welcome brief presentations, but also plan to spend time in discussion.
|5:30pm||meet in MBB atrium, go to dinner ("Dutch" treat)|
|7:15pm||Moonlight and Magnolias, $10|
ACU's production of the comedy Moonlight and Magnolias by Ron Hutchinson will be presented on campus. We have a block of seats reserved for Friday night at 7:30PM for those interested. Just let us know when you register; the cost for the show is $10.
|8:30||Predicate-Based Testing, Verification, and other Formal Methods in the Undergraduate Computer Science Curriculum, Rex Page, OU|
|9:20||A paradigm for semi-formal proofs, Nelson Rushton, TTU|
|10:10||An Open Fortress, Eric Allen, Sun|
|11:00||Automated Parallelisms from SequenceL Specifications, Dan Cooke, TTU|
|11:50||BBQ lunch (provided)|
|break, conversation, walk/tour, whatever|
|1:10||Strategic Programming by Model Interpretation and Partial Evaluation, William Cook, UT Austin|
|2:00||Domain Specific Languages, Walid Taha, Rice|
|2:50||Java Type Inference Is Broken: Can We Fix It?, Dan Smith, Rice|
|3:40||wrap up, planning for next meeting|
Presentations will be 30 minutes or less to allow time for participants to ask questions, make comments or discuss the material presented.
Please register by August 29 so we can plan for lunch. Send your name, affiliation, and contact information to Dwayne Towell.
Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.
In this talk, I dissect the type inference algorithm of Java 5 and propose a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower- bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. It is hoped that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.
We describe a paradigm of mathematical argument intermediate between formal proofs (a la Frege, Gentzen, etc.) and traditional prose proofs (a la Euclid), which leaves inference rules as a free parameter while giving formal guidelines for the structure of arguments. We present a shorthand for writing proofs in this framework which preserve much of the look and feel of traditional prose proofs. Arguments in this format can be read using a software assistant that presents the reader with individual inferences in isolation, and automatically verifies the Boolean algebra that links the inferences together into an argument. We hypothesize the system facilitates greater accuracy in checking proofs (compared with prose). We also hope that it gives students a mental model for proofs which has formal structure and properties, and yet which meshes with their experience of proofs they normally see in their textbooks and in class.
Strategic Programming is a programming paradigm based on factoring programs into general strategies applied to descriptions of particular application requirements. The descriptions are called models, and they generally describe one aspect of an application. Parser generators (like Yacc) are a prototypical example of strategic programming. My talk focuses on defining the semantics of models using interpreters instead of transformations, as in most related work. It is possible to define fully-functional applications by a collection of interrelated models for different aspects of a system, including user interface, security, workflow, data abstraction and persistence. The models may also contain fragments of code written in general-purposes languages. Model interpreters are compiled by partial evaluation. One novelty of this approach is the ability to create data abstractions by model interpretation and compile them by partial evaluation. I will describe my progress in implementing a software development toolset to support strategic programming by model interpretation and partial evaluation. The system is implemented in itself and is targeted at information management applications, including desktop, web and distributed services, although it may be applicable to other domains as well.
What would it mean to claim that an implementation of a function that packages a sequence into its non-overlapping, contiguous subsequences of a specified length is correct? One approach is to express properties that a programmer might test for when building the implementation. These properties could be expressed as formulas in symbolic logic. Since the formulas would involve other functions, correctness would be relative to those functions, and their properties would need to be assumed, if they were basic elements of the programming language, or verified if not. This talk will present a model of correctness for an ACL2 implementation of the aforementioned packaging function and its supporting functions, along with verification of the model using the ACL2 theorem prover.
Two years ago, the Fortress Project at Sun Labs was turned into an open source project: Daily revisions to the Fortress code base have been publicly visible, external developers have been granted commit privileges, and many technical discussions on the direction of the implementation have been conducted openly and with participation by external developers. In March of this year, Fortress has taken its next leap forward with the release of Fortress 1.0: The first specification of the language that has been synchronized with the the implementation. With this release, the Fortress community is better able to evaluate the design of new features, users are better able to use them, and developers are better able to contribute to the implementation, as they can now work off of a stable and well- specified code base. In this talk, I review the benefits and challenges we have had in working on Fortress in the open, and our plans for growing the language in the future.