Modern type systems (eg in Haskell and ML) exclude many bugs by construction. But not all! We would like to go beyond these type systems, and write down the pre and post-conditions of our functions. More generally, in a higher-order language like Haskell, we extend traditional pre/post conditions to so-called "contracts.
Then we are faced with questions likeIn my talk I'll describe work in progress that makes some progress on these questions, in the context of Haskell. Our goal is to extend the "reach" of static verification, beyond traditional type systems, and to do so in a way that ordinary programmers (without PhDs) can make sense of.
- What does it mean, precisely, for a function to 'satisfy a contract'?
- How can we statically verify that it satisfies the contract?
- What if the contract itself violates the contracts of the functions it calls?
15:00h-15:30h Coffee
15:30h-16:30h
Geometry of Synthesis: A structured approach to VLSI design
Dan Ghica, University of Birmingham
Related
paper.
I propose a new technique for hardware synthesis from higher-order functional languages with imperative features based on Reynolds's Syntactic Control of Interference. The affine type system is useful for managing the thorny issue of sharing in physical circuits. We use a semantic model inspired by game semantics and the geometry of interaction, and express it directly as a certain class of digital circuits that form a cartesian, monoidal-closed category. Based on this theoretical foundation we introduce a new ANSI C to hardware compiler and we discuss some methodological issues regarding the role of higher order programming languages in hardware design.
16:30h-17:30h
Switched-on Yampa: Programming Modular Synthesizers in Haskell
Henrik Nilsson, University of Nottingham
Slides
In this talk and demonstration, we present an implementation of a modular synthesizer in Haskell using Yampa. A synthesizer, be it a hardware instrument or a pure software implementation, as here, is said to be modular if it provides sound-generating and sound-shaping components that can be interconnected in arbitrary ways. Yampa, a Haskell-embedded implementation of Functional Reactive Programming, supports flexible construction of hybrid systems. Since music is a hybrid continuous-time and discrete-time phenomenon, Yampa and is a good fit for such applications, offering some unique possibilities compared to most languages targeting music or audio applications. The demonstration illustrates this point by showing how simple audio blocks can be described and then interconnected in a network with dynamically changing structure, reflecting the changing demands of a musical performance.
Page maintained by E.Ritter@cs.bham.ac.uk