Wednesday, 10th February 2010, 13:00 – 17:30
ICMS, 14 India Street, Edinburgh
India Street is situated in the New Town district of Edinburgh
which is just to the north of the city centre, a few minutes
walk from Haymarket or Waverley train stations.
(Location map from GoogleMaps)
| 12:00 | Lunch | |
| 12:55 |
Hans-Wolfgang Loidl, Heriot-Watt University Announcement: SICSA MultiCore Challenge |
|
| 13:00 |
Edwin Brady, University of St Andrews Implementing Domain Specific Languages using Dependent Types and Partial Evaluation In this talk, I will describe the efficient implementation of domain specific languages (DSLs) in Idris, a dependently typed functional programming language. I will introduce the language Idris, and show how it can be used to implement a verified network transport protocol, as a DSL. I will present experimental evidence that partial evaluation of such programs yields efficient residual programs whose performance is competitive with their Java and C equivalents and which are also, through the use of dependent types, verifiably type- and resource-safe. |
|
| 13:40 |
Bob Atkey, University of Strathclyde Amortised Resource Analysis with Separation Logic Type-based amortised resource analysis following Hofmann and Jost — where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline — have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative languages by embedding a logic of resources, based on Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the resources associated with each member of the structure. We present the logic on a small imperative language with procedures and mutable heap, based on Java bytecode. We have formalised the logic within the Coq proof assistant and extracted a certified verification condition generator. We demonstrate the logic on some examples, including proving termination of in-place list reversal on lists with cyclic tails. |
|
| 14:20 |
Lenore M. Mullin, University at Albany, State University of New York Optimization of Tensor Based Languages The pervasiveness of matrix decompositions and tensor operations in knowledge representation, and the sciences: biological, chemical, physical, ... ([1, 2]) have renewed an interest in domain specific algorithms. Consequently, there also exists a renewed interest in domain specific computing: libraries (Flame), languages (Spiral), symbolic/numeric computing, expression templates, compilers, operating systems, and processor/memory hierarchies. The transformational nature of matrix (2-d tensors) operations and tensor operations in general, provides a prudent, hopeful, and deterministic way to reason about computation. The determinism arises from the data structure, i.e. memory layout (contiguous), and the linear (and multilinear) operations applied to the data structure. It also comes from using the same tensor operations to abstract the processor/memory/network hierarchy. This talk will discuss how to optimize multiple Kronecker Products using A Mathematics of Arrays and Psi Calculus, an algebra of multi-dimensional arrays and an index calculus. References:
|
|
| 15:00 | Tea/Coffee | |
| 15:30 |
Philip Wadler, University of Edinburgh The Audacity of Hope: Thoughts on Reclaiming the Database Dream A venerable line of research aims to provide a general-purpose programming language with a well-defined subset that compiles into efficient queries, perhaps by translation into SQL or some other suitable query language. This talk discusses some older and more recent advances in this direction, including the languages Kleisli, LINQ, Ferry, M, and Links. |
|
| 16:10 |
Neil Ghani, University of Strathclyde All Initial Algebras Support Induction We know that all initial algebras, solely from initiality, support recursive definitions. These are known as folds in the FP community. But, so far, it seems that only certain classes of initial algebras support proof by induction. This is an asymmetry and it is displeasing. I'll show how we can restore the harmony that the universe seeks. Namely, I'll show that all initial algebras, solely from their initiality, support proof by induction. This is joint work with Patricia Johann. |
|
| 16:50 |
Michael Gabbay, King's College London A Simple Class Of Kripke-Style Models In Which Logic And Computation Have Equal Standing We present a sound and complete model of lambda-calculus reductions based on structures inspired by modal logic (closely related to Kripke structures). Accordingly we can construct a logic which is sound and complete for the same models, and we identify lambda-terms with certain simple sentences (predicates) in this logic, by direct compositional translation. Under this identification, reduction becomes identified with logical entailment. Thus, the models suggest a new way to identify logic and computation. Both have elementary and concrete representations in our models; where these representations overlap, they coincide. In a concluding speculation, we note a certain subclass of the models which seems to play a role analogous to that played by the cumulative hierarchy models in axiomatic set theory and the natural numbers in formal arithmetic — there are many models of the respective theories, but only some, characterised by a fully second order interpretation, are the `intended' ones. |
|
| 17:30 | Pub — probably The Oxford Bar |
This meeting of SPLS has received financial support from the Complex Systems Engineering theme of SICSA, the Scottish Informatics and Computer Science Alliance.
General information about the SPLS series can be found on the SPLS page. For information about this event contact the organisers:
School of Mathematical and Computer Sciences, Heriot-Watt University