12th Symposium on Programming Languages and Software Tools - SPLST'11

Tallinn, Estonia, October 5-7, 2011


"Why Dependent Types Matter"

Thorsten Altenkirch, School of Computer Science, University of Nottingham, UK

Abstract. Dependent types are types which depend on values allowing us to talk about sequences of a fixed length, square matrices and many other things we want to say about a computation. As a consequence computations itself find their way into the types, astutely compared to the ”proletarian revolution” by McBride.

Dependent types indeed revolutionize the nature of programming by reaching a limit of expressibility allowing us to say whatever we want to say about a program in its type; and checkable by a compiler instead of being hidden in comments inaccessible by the machine. This is achieved without artificially putting on a logical superstructure on a programming language but by just extending the use of types in a natural way. Thus we can freely move along the axis from prototype to verified system and pay as we go.

Opportunity doesn’t come without challenges: the design space for dependently typed programming languages is huge. The language Agda is now a vehicle for experiments with dependently typed programming. I will use Agda to illustrate the potential of dependently typed programming to express complex data dependency, to eliminate run-time errors and to integrate logic and programming using the Curry-Howard equivalence. At the same time we shall have a glimpse at the huge design space for dependently typed languages which we will have to navigate if we want to make the power of dependent types available to ordinary programmers.


"Answer Set Programming: A Declarative Approach to Solving Challenging Search Problems"

Ilkka Niemelä, Department of Information and Computer Science, Aalto University, Finland

Abstract. Answer set programming (ASP) is a declarative programming paradigm that has its roots in the stable model (answer set) semantics of logic programs and implementations of this semantics developed in the late 90's. The basic idea of ASP is similar to, for example, SAT-based planning or constraint satisfaction problems but in ASP the goal is to provide a more powerful knowledge representation language for effective problem encoding. A number of successful ASP systems have already been developed and applied in areas such as planning, decision support for the flight controllers of space shuttles, web-based product configuration, configuration of a Linux distribution, computer aided verification, VLSI routing, network management, security protocol analysis, network inhibition analysis, and diagnosis.

The talk explains the theoretical underpinnings of ASP, introduces the ASP programming paradigm, outlines computational techniques used in current ASP solvers, and discusses some interesting applications of the approach.


"Component reuse in ensemble-based medical image processing applications"

András Hajdu and Bálint Antal, Department of Computer Graphics and Image Processing, University of Debrecen, Hungary

Abstract. In this paper, we propose a meta-level component reuse approach. We not only reuse components, but also form automatically a new algorithm from them. As another contribution, we also show that an ensemble can also be formed from these new algorithms, which is another level of component reuse. We show a case study, namely microaneurysm detection in color fundus images to show the practical use of this approach. This application is tested in an international online competition with promising results.

Valid CSS! Valid XHTML 1.0 Strict Last changed September 23, 2011 14:40 EET by local organizers, splst11(at)cs.ioc.ee
SPLST'11 page: http://cs.ioc.ee/splst11/