Abstracts and BibTeX entries

Lazy algorithmic debugging: ideas for practical implementation

Lazy functional languages have non-strict semantics and are purely declarative, i.e. they support the notion of referential transparency and are devoid of side effects. Traditional debugging techniques are, however, not suited for lazy functional languages since computations generally do not take place in the order one might expect. Since algorithmic debugging allows the user to concentrate on the declarative aspects of program semantics, and will semi-automatically find functions containing bugs, we propose to use this technique for debugging lazy functional programs. Our earlier work showed that this is a promising approach. However, the current version of our debugger has severe implementational problems, e.g. too large trace size and too many questions asked. This paper suggests a number of techniques for overcoming these problems, at least partially. The key techniques are immediate strictification and piecemeal tracing.

@InProceedings{Nilsson1993,
  author =       "Henrik Nilsson and Peter Fritzson",
  title =        "Lazy Algorithmic Debugging: Ideas for Practical
                 Implementation",
  editor =       "Peter Fritzson",
  volume =       "749",
  series =       "Lecture Notes in Computer Science",
  pages =        "117--134",
  booktitle =    "Automated and Algorithmic Debugging",
  year =         "1993",
  address =      "Link\"{o}ping, Sweden",
  month =        may
}


Algorithmic debugging for lazy functional languages

Lazy functional languages have non-strict semantics and are purely declarative, i.e. they support the notion of referential transparency and are devoid of side effects. Traditional debugging techniques are, however, not suited for lazy functional languages since computations generally do not take place in the order one might expect. Since algorithmic debugging allows the user to concentrate on the declarative aspects of program semantics, and will semi-automatically find functions containing bugs, we propose to use this technique for debugging lazy functional programs. Because of the non-strict semantics of lazy functional languages, arguments to functions are in general partially evaluated expressions. The user is, however, usually more concerned with the values that these expressions represent. We address this problem by providing the user with a strictified view of the execution trace whenever possible. In this paper we present an algorithmic debugger for a lazy functional language based on strictification and some experience in using it. A number of problems with the current implementation of the debugger, e.g. too large trace size and too many questions asked, are also discussed and some techniques for overcoming these problems, at least partially, are suggested, the key techniques being immediate strictification and piecemeal tracing.

@Article{Nilsson1994,
  author = 	 "Henrik Nilsson and Peter Fritzson",
  title = 	 "Algorithmic Debugging for Lazy Functional Languages",
  journal =	 "Journal of Functional Programming",
  year =	 1994,
  volume =	 4,
  number =	 3,
  pages =        "337--370",
  month =	 jul
}


A declarative approach to debugging for lazy functional languages

Debugging programs written in lazy functional languages is difficult, and there are currently no realistic, general purpose debugging tools available. The basic problem is that computations in general do not take place in the order one might expect. Furthermore, lazy functional languages to a large extent free programmers from concerns regarding operational issues such as evaluation order, i.e. they are declarative. Debugging should therefore take place at the same, high level of abstraction. Thus, we propose to use algorithmic debugging for lazy functional languages, since this technique allows the user to focus on the declarative semantics of a program.

However, algorithmic debugging is based on tracing, and since the trace reflects the operational behaviour of the traced program, the trace should be transformed to abstract away these details if we wish to debug as declaratively as possible. We call this transformation strictification, because it makes the trace more like a trace from a strict language.

In this thesis, we present a strictifying algorithmic debugger for a small lazy functional language, and some experience from using it. We also discuss its main shortcomings, and outline a number of ideas for building a more realistic debugger. The single most pressing problem is the size of a complete trace. We propose to use a piecemeal tracing scheme to overcome this, by which only a part of the trace is stored at any one time, other parts being created on demand by re-executing the program.

@MastersThesis{Nilsson1994b,
  author = 	 "Henrik Nilsson",
  title = 	 "A Declarative Approach to Debugging for Lazy
		  Functional Languages",
  school = 	 "Department of Computer and Information Science,
                 {Link\"{o}ping} University",
  year = 	 1994,
  address =	 "S-581 83, {Link\"{o}ping}, Sweden",
  month =	 sep,
  type =	 "{L}icentiate {T}hesis {N}o. 450"
}


The architecture of a debugger for lazy functional languages

Debugging programs written in lazy functional languages is difficult, and there are currently no realistic, general purpose debugging tools available. The basic problem is that computations in general do not take place in the order one might expect. Furthermore, lazy functional languages are `declarative'. Hence it is advantageous if debugging takes place at the same, high level of abstraction. Thus, we propose to base debugging on what we call Evaluation Dependence Trees (EDT), which reflect the declarative semantics of the programs rather than operational concerns such as evaluation order. This in turn naturally suggests a two level debugger architecture where the lower level generates the EDT and the upper level allows the user to investigate it. The main advantage of this is flexibility: components realizing the two levels may be chosen independently to suit the debugging problem at hand.

@InProceedings{Sparud1995,
  author = 	 "Jan Sparud and Henrik Nilsson",
  title = 	 "The Architecture of a Debugger for Lazy Functional
		  Langauges",
  editor =	 "Mireille Ducass\'{e}",
  booktitle =	 "Proceedings of {AADEBUG '95}, 2nd International
		  Workshop on Automated and Algorithmic Debugging",
  year =	 1995,
  organization = "{IRISA}, Campus Universitaire de Beaulieu, 35042 Rennes,
		  Cedex, France",
  address =	 "Saint-Malo, France",
  month =	 may
}


The evaluation dependence tree: an execution record for lazy functional debugging

Lazy functional languages are declarative and allow the programmer to write programs where operational issues such as the evaluation order are left implicit. This should be reflected in the design of debuggers for such languages to avoid burdening the programmer with operational details, e.g. concerning the actual evaluation order. Conventional debugging techniques tend to focus too much on operational aspects to be suitable in this context. A record of the execution that only captures the declarative aspects of the execution, leaving out operational details, would be a viable basis for debugging lazy functional programs. Various declarative debugging tools could then be developed on top of such records. In this paper we propose a structure which we call the Evaluation Dependence Tree (EDT) for this purpose, and we describe two different construction methods. Performance problems are discussed along with possible solutions, and some performance figures from experiments in a realistic context are given.

@TechReport{Nilsson1996,
  author = 	 "Henrik Nilsson and Jan Sparud",
  title = 	 "The Evaluation Dependence Tree: an Execution Record
		  for Lazy Functional Debugging",
  institution =  "Department of Computer and Information Science,
                 {Link\"{o}ping} University",
  year = 	 1996,
  type =	 "Research Report",
  number =	 "{LiTH-IDA-R-96-23}",
  address =	 "S-581 83, {Link\"{o}ping}, Sweden",
  note =         "This is an extended version of \cite{Nilsson97}.",
  month =	 aug
}


The evaluation dependence tree as a basis for lazy functional lazy functional debugging

Lazy functional languages are declarative and allow the programmer to write programs where operational issues such as the evaluation order are left implicit. This should be reflected in the design of debuggers for such languages to avoid burdening the programmer with operational details, e.g. concerning the actual evaluation order. Conventional debugging techniques tend to focus too much on operational aspects to be suitable in this context. A record of the execution that only captures the declarative aspects of the execution, leaving out operational details, would be a viable basis for debugging lazy functional programs. Various declarative debugging tools could then be developed on top of such records. In this paper we propose a structure which we call the Evaluation Dependence Tree (EDT) for this purpose, and we describe two different construction methods. Performance problems are discussed along with possible solutions.

@Article{Nilsson1997,
  author = 	 "Henrik Nilsson and Jan Sparud",
  title = 	 "The Evaluation Dependence Tree as a Basis for Lazy
		  Functional Debugging",
  journal =	 "Automated Software Engineering",
  year =	 1997,
  volume =	 4,
  number =	 2,
  pages =	 "121--150",
  month =	 apr
}


Declarative debugging for lazy functional languages

Lazy functional languages are declarative and allow the programmer to write programs where operational issues such as the evaluation order are left implicit. It is desirable to maintain a declarative view also during debugging so as to avoid burdening the programmer with operational details, for example concerning the actual evaluation order which tends to be difficult to follow. Conventional debugging techniques focus on the operational behaviour of a program and thus do not constitute a suitable foundation for a general-purpose debugger for lazy functional languages. Yet, the only readily available, general-purpose debugging tools for this class of languages are simple, operational tracers.

This thesis presents a technique for debugging lazy functional programs declaratively and an efficient implementation of a declarative debugger for a large subset of Haskell. As far as we know, this is the first implementation of such a debugger which is sufficiently efficient to be useful in practice. Our approach is to construct a declarative trace which hides the operational details, and then use this as the input to a declarative (in our case algorithmic) debugger.

The main contributions of this thesis are:

This work has been supported by the Swedish National Board for Industrial and Technical Development (NUTEK).

@PhdThesis{Nilsson1998,
  author = 	 "Henrik Nilsson",
  title = 	 "Declarative Debugging for Lazy Functional Languages",
  school = 	 "Department of Computer and Information Science,
                 {Link\"{o}pings universitet}",
  year = 	 1998,
  address =	 "S-581 83, {Link\"{o}ping}, Sweden",
  month =	 may,
  type =	 "{PhD} thesis"
}


Tracing piece by piece: affordable debugging for lazy functional languages

The advantage of lazy functional languages is that programs may be written declaratively without specifying the exact evaluation order. The ensuing order of evaluation can however be quite involved which makes it difficult to debug such programs using traditional, operational techniques. A solution is to trace the computation in a way which focuses on the declarative aspects and hides irrelevant operational details. The main problem with this approach is the immense cost in time and space of tracing large computations. Dealing with these performance issues is thus the key to practical, general purpose debuggers for lazy functional languages. In this paper we show that computing partial traces on demand by re-executing the traced program is a viable way to overcome these difficulties. This allows any program to be traced using only a fixed amount of extra storage. Since it takes a lot of time to build a complete trace, most of which is wasted since only a fraction of a typical trace is investigated during debugging, partial tracing and repeated re-execution is also attractive from a time perspective. Performance figures are presented to substantiate our claims.

This work has been supported by the Swedish National Board for Industrial and Technical Development (NUTEK) and by the Wenner-Gren Foundations, Stockholm, Sweden.

@InProceedings{Nilsson1999,
  author = 	 "Henrik Nilsson",
  title = 	 "Tracing piece by piece: affordable debugging for
		  lazy functional languages",
  pages =	 "36--47",
  booktitle =	 "Proceedings of the 1999 {ACM SIGPLAN} international
		  conference on Functional programming",
  year =	 1999,
  publisher =	 "{ACM} Press",
  address =	 "Paris, France",
  month =	 sep
}


From executable formal specification to Java property verification

In this extended abstract, we describe our work on an executable, dynamic semantic specification for a significant subset of Java, including exceptions and multi-threading. The dynamic semantics is expressed in natural semantics using the formalism Typol. A dedicated, graphical, programming environment has been generated from the dynamic semantics and a specification of the Java syntax using the Centaur environment, thus allowing the semantics to be tested extensively on real Java programs. This in turn allowed many errors to be fixed, and we now believe that the specification is reasonably correct. The next step is to formally prove the correctness of central aspects of the semantics. We focus on multi-threading aspects and their interaction with the control flow (e.g. exceptions). While this is work in progress, we sketch such a proof in this extended abstract.

@InProceedings{Attali2000a,
  author = 	 "Isabelle Attali and Denis Caromel and Henrik Nilsson
                  and Marjorie Russo",
  title = 	 "From Executable Formal Specification to {J}ava Property
                  Verification",
  booktitle = 	 "Second {ECOOP} Workshop on Formal Techniques for Java
                  Programs",
  pages =	 "1--7",
  year =	 2000,
  organization = "{INRIA} Sophia Antipolis",
  address =	 "Sophia Antipolis, France",
  month =	 jun,
}


Smart tools for Java cards

This article describes a Java Card programming environment which to a large extent is generated from formal specifications of the syntax and semantics of Java Card, the JCRE (Java Card Runtime Environment), and the Java Card APIs. The resulting environment consists of a set of tightly integrated and somewhat smart tools, such as a Java specific structure editor and a simulator which allows an application to be tested before being downloaded to a card. Furthermore, the simulator analyses the applet in question in order to find out the structure of the accepted commands. This information is then used to automatically adapt the GUI of the simulator.

This work was partially financed by Bull. Henrik Nilsson was supported by a post doctoral grant from the Wenner-Gren Foundations, Stockholm, Sweden.

@InProceedings{Attali2000b,
  author = 	 "Isabelle Attali and Denis Caromel and Carine Courbis and
                  Ludovic Henrio and Henrik Nilsson",
  title = 	 "Smart Tools for {J}ava Cards",
  editor =	 "Josep Domingo-Ferrer and David Chan and Anthony Watson",
  booktitle =	 "Smart Card Research and Advanced Applications",
  year =	 2000,
  publisher =	 "Kluwer Academic Publishers",
  month =	 sep,
  note =	 "Proceedings of the {IFIP} Fourth Working Conference
		  on Smart Card Research and Advanced Applications
		  ({CARDIS} 2000), {HP} Labs, Bristol, {UK}"
}


An integrated development environment for Java Card

This article describes a Java Card programming environment which to a large extent is generated from formal specifications of the syntax and semantics of Java Card, the JCRE (Java Card Runtime Environment), and the Java Card APIs. The resulting environment consists of a set of tightly integrated and somewhat smart tools, such as a Java specific structure editor and a simulator which allows an application to be tested before being downloaded to a card. Furthermore, the simulator analyses the applet in question in order to find out the structure of the accepted commands. This information is then used to automatically adapt the GUI of the simulator.

This work was partially financed by Bull. Henrik Nilsson was supported by a post doctoral grant from the Wenner-Gren Foundations, Stockholm, Sweden.

@Article{Attali2001,
  author =       "Isabelle Attali and Denis Caromel and Carine Courbis and
                  Ludovic Henrio and Henrik Nilsson",
  title =        "An Integrated Development Environment for {Java Card}",
  journal =      "Computer Networks",
  pages =        "391--405",
  year =         2001,
  volume =       36,
  number =       4,
  month =        jul
}


How to look busy while being as lazy as ever: the implementation of a lazy functional debugger

This article describes the implementation of a debugger for lazy functional languages like Haskell. The key idea is to construct a declarative trace which hides the operational details of lazy evaluation. However, to avoid excessive memory consumption, the trace is constructed one piece at a time, as needed during a debugging session, by automatic re-execution of the program being debugged. This article gives a fairly detailed account of both the underlying ideas and of our implementation. It also presents performance figures which demonstrate the feasibility of the approach.

This work has been supported by the Swedish Board for Industrial and Technical Development (NUTEK) and by the Wenner-Gren Foundations, Stockholm, Sweden.

@Article{Nilsson2001,
  author =       "Henrik Nilsson",
  title =        "How to Look Busy while Being as Lazy as Ever: The
                  Implementation of a Lazy Functional Debugger",
  journal =      jfp,
  year =         2001,
  volume =       11,
  number =       6,
  pages =        "629--671",
  month =        nov
}


Functional reactive programming, continued

Functional Reactive Programming (FRP) extends a host programming language with a notion of time flow. Arrowized FRP (AFRP) is a version of FRP embedded in Haskell based on the arrow combinators. AFRP is a powerful synchronous dataflow programming language with hybrid modeling capabilities, combining advanced synchronous dataflow features with the higher-order lazy functional abstractions of Haskell. In this paper, we describe the AFRP programming style and our Haskell-based implementation. Of particular interest are the AFRP combinators that support dynamic collections and continuation-based switching. We show how these combinators can be used to express systems with an evolving structure that are difficult to model in more traditional dataflow languages.

@InProceedings{Nilsson2002a,
  author =       "Henrik Nilsson and Antony Courtney and John Peterson",
  title =        "Functional Reactive Programming, Continued",
  booktitle =    "Proceedings of the 2002 {ACM SIGPLAN} {H}askell
                  Workshop ({H}askell'02)",
  pages =        "51--64",
  year =         2002,
  address =      "Pittsburgh, Pennsylvania, USA",
  publisher =    "{ACM} Press",
  month =        oct
}


System presentation - Functional reactive robotics: an excercise in principled integration of domain-specific languages

Software for (semi-) autonomous robots tends to be a complex combination of components from many different application domains such as control theory, vision, and artificial intelligence. Components are often developed using their own domain-specific tools and abstractions. System integration can thus be a significant challenge, in particular when the application calls for a dynamic, adaptable system structure in which rigid boundaries between the subsystems are a performance impediment. We believe that, by identifying suitably abstract notions common to the different domains in question, it is possible to create a broader framework for software integration and to recast existing domain-specific frameworks in these terms. This approach simplifies integration and leads to improved reliability. In this paper, we show how Functional Reactive Programming (FRP) can serve as such a unifying framework for programming vision-guided, semi-autonomous robots and illustrate the benefits this approach entails. The key abstractions in FRP, reactive components describing continuous or discrete behavior in a declarative style, are first class entities, allowing the resulting systems to exhibit a dynamic, adaptable structure which we regard as especially important in the area of autonomous robots.

@InProceedings{Pembeci2002,
  author =       "Izzet Pembeci and Henrik Nilsson and Greogory Hager",
  title =        "System Presentation -- Functional Reactive Robotics: An
                  Exercise in Principled Integration of Domain-Specific
                  Languages",
  pages =        "168--179",
  booktitle =    "Principles and Practice of Declarative Programming
                  ({PPDP'02})",
  year =         2002,
  address =      "Pittsburgh, Pennsylvania, USA",
  month =        oct
}


Functional hybrid modeling

The modeling and simulation of physical systems is of key importance in many areas of science and engineering, and thus can benefit from high-quality software tools. In previous research we have demonstrated how functional programming can form the basis of an expressive language for causal hybrid modeling and simulation. There is a growing realization, however, that a move toward non-causal modeling is necessary for coping with the ever increasing size and complexity of modeling problems. Our goal is to combine the strengths of functional programming and non-causal modeling to create a powerful, strongly typed fully declarative modeling language that provides modeling and simulation capabilities beyond the current state of the art. Although our work is still in its very early stages, we believe that this paper clearly articulates the need for improved modeling languages and shows how functional programming techniques can play a pivotal role in meeting this need.

@InProceedings{Nilsson2003a,
  author =       "Henrik Nilsson and John Peterson and Paul Hudak",
  title =        "Functional Hybrid Modeling",
  booktitle =    "Proceedings of {PADL'03}: 5th International Workshop on
                  Practical Aspects of Declarative Languages",
  pages =        "376--390",
  year =         2003,
  volume =       2562,
  series =       lncs,
  address =      "New Orleans, Lousiana, USA",
  month =        jan,
  publisher =    sv
}


Arrows, robots, and functional reactive programming

Functional reactive programming, or FRP, is a paradigm for programming hybrid systems -- i.e., systems containing a combination of both continuous and discrete components -- in a high-level, declarative way. The key ideas in FRP are its notions of continuous, time-varying values, and time-ordered sequences of discrete events. Yampa is an instantiation of FRP as a domain-specific language embedded in Haskell. This paper describes Yampa in detail, and shows how it can be used to program a particular kind of hybrid system: a mobile robot. Because performance is critical in robotic programming, Yampa uses arrows (a generalization of monads) to create a disciplined style of programming with time-varying values that helps ensure that common kinds of time- and space-leaks do not occur. No previous experience with robots is expected of the reader, although a basic understanding of physics and calculus is assumed. No knowledge of arrows is required either, although we assume a good working knowledge of Haskell.

@InProceedings{Hudak2003,
  author =       "Paul Hudak and Antony Courtney and Henrik Nilsson
                  and John Peterson",
  title =        "Arrows, Robots, and Functional Reactive Programming",
  booktitle =    "Summer School on Advanced Functional Programming 2002, 
                  Oxford University",
  year =         2003,
  volume =	 2638,
  series =       "Lecture Notes in Computer Science",
  pages =        "159--187"
  publisher =    "Springer-Verlag"
}


Functional Automatic Differentiation with Dirac Impulses

Functional Reactive Programming (FRP) is a framework for reactive programming in a functional setting. FRP has been applied to a number of domains, such as graphical animation, graphical user interfaces, robotics, and computer vision. Recently, we have been interested in applying FRP-like principles to hybrid modeling and simulation of physical systems. As a step in that direction, we have extended an existing FRP implementation, Yampa, in two new ways that make it possible to express certain models in a very natural way, and reduces the amount of work needed to put modeling equations into a suitable form for simulation. First, we have added Dirac impulses that allow certain types of discontinuities to be handled in an easy yet rigorous manner. Second, we have adapted automatic differentiation to the setting of Yampa, and generalized it to work correctly with Dirac impulses. This allows derivatives of piecewise continuous signals to be well-defined at all points. This paper reviews the basic ideas behind automatic differentiation, in particular Jerzy Karczmarczuk's elegant version for a lazy functional language with overloading, and then considers the integration with Yampa and the addition of Dirac impulses.

@InProceedings{Nilsson2003b,
  author =       "Henrik Nilsson",
  title =        "Functional Automatic Differentiation with {D}irac Impulses",
  booktitle =    "Proceedings of the Eighth {ACM} {SIGPLAN} International
                  Conference on Functional Programming",
  pages =        "153--164",
  year =         2003,
  address =      "Uppsala, Sweden",
  month =        aug,
  publisher =    "{ACM} Press"
}


The Yampa Arcade

Simulated worlds are a common (and highly lucrative) application domain that stretches from detailed simulation of physical systems to elaborate video game fantasies. We believe that Functional Reactive Programming (FRP) provides just the right level of functionality to develop simulated worlds in a concise, clear and modular way. We demonstrate the use of FRP in this domain by presenting an implementation of the classic "Space Invaders" game in Yampa, our most recent Haskell-embedded incarnation of FRP.

@InProceedings{Courtney2003b,
  author =       "Antony Courtney and Henrik Nilsson and John Peterson",
  title =        "The {Y}ampa Arcade",
  booktitle =    "Proceedings of the 2003 {ACM SIGPLAN} {H}askell
                  Workshop ({H}askell'03)",
  pages =        "7--18",
  year =         2003,
  address =      "Uppsala, Sweden",
  publisher =    "{ACM} Press",
  month =        aug
}


Haskell '04: Proceedings of the 2004 ACM SIGPLAN workshop on Haskell

It is my great pleasure to welcome you to the ACM SIGPLAN 2004 Haskell Workshop. The purpose of the Haskell Workshop is to discuss experience with Haskell, and possible future developments for the language. The scope of the workshop includes all aspects of the design, semantics, theory, application, implementation, and teaching of Haskell.The 2004 Haskell Workshop takes place on 22 September, 2004, in Snowbird, Utah, USA, in affiliation with the 2004 International Conference on Functional Programming (ICFP'04). The call for papers attracted 27 submissions. Each paper was evaluated by at least three international referees. During a five-day electronic meeting, the program committee selected nine of the submissions for presentation at the workshop as full papers based on the referee reports. The program committee also selected a student paper for a short presentation. Additionally, two tool demonstrations, the abstracts of which are included in these proceedings, were selected from five proposals. The 2004 workshop program also includes the annual The Future of Haskell discussion.

@Proceedings{Nilsson2004,
  title = 	 "{H}askell '04: Proceedings of the 2004 {ACM SIGPLAN}
                   workshop on {H}askell",
  year = 	 2004,
  editor =	 "Henrik Nilsson",
  address =	 "Snowbird, Utah, USA",
  publisher =	 "ACM",
  annote =	 "ISBN: 1-58113-850-4"
}


Dynamic Optimization for Functional Reactive Programming using Generalized Algebraic Data Types

A limited form of dependent types, called Generalized Algebraic Data Types (GADTs), has recently been added to the list of Haskell extensions supported by the Glasgow Haskell Compiler. Despite not being full-fledged dependent types, GADTs still offer considerably enlarged scope for enforcing important code and data invariants statically. Moreover, GADTs offer the tantalizing possibility of writing more efficient programs since capturing invariants statically through the type system sometimes obviates entire layers of dynamic tests and associated data markup. This paper is a case study on the applications of GADTs in the context of Yampa, a domain-specific language for Functional Reactive Programming in the form of a self-optimizing, arrow-based Haskell combinator library. The paper has two aims. Firstly, to explore what kind of optimizations GADTs make possible in this context. Much of that should also be relevant for other domain-specific embedded language implementations, in particular arrow-based ones. Secondly, as the actual performance impact of the GADT-based optimizations is not obvious, to quantify this impact, both on tailored micro benchmarks, to establish the effectiveness of individual optimizations, and on two fairly large, realistic applications, to gauge the overall impact. The performance gains for the micro benchmarks are substantial. This implies that the Yampa API could be simplified as a number of "pre-composed" primitives that were there mainly for performance reasons are no longer needed. As to the applications, a worthwhile performance gain was obtained in one case whereas the performance was more or less unchanged in the other.

@InProceedings{Nilsson2005a,
  author = 	 "Henrik Nilsson",
  title = 	 "Dynamic Optimization for Functional Reactive
                  Programming using Generalized Algebraic Data Types",
  booktitle = 	 "Proceedings of the Tenth {ACM} {SIGPLAN} International
                  Conference on Functional Programming (ICFP'05)",
  pages =	 "54--65"
  year =	 2005,
  address =	 "Tallinn, Estonia",
  month =	 sep,
  publisher =	 "{ACM} Press"
}


Type-theoretic design patterns

The development of design patterns in object-oriented programming aims at capturing good software design in a reusable generic form. However, design patterns are not expressible in conventional object-oriented programming languages. To address this shortcoming, we need to model and understand design patterns precisely. We achieve this by identifying operators characterising the most fundamental design patterns in a way that enables the construction of object-oriented programs with provable structural and behavioural properties. We use dependent-type theory to define a simplified, functional model of object-oriented programming. Design patterns are modelled in this setting as operators on object signatures and implementations. We present examples of several basic design operators and design patterns modelled in this setting and show how properties of their composition can be proven.

@InProceedings{Rypacek2006,
  author = 	 "Ond\v{r}ej Ryp\'{a}\v{c}ek and Roland Backhouse and Henrik
                  Nilsson",
  title = 	 "Type-theoretic design patterns",
  booktitle = 	 "Proceedings of the 2006 ACM SIGPLAN Workshop on Generic
                  Programming",
  pages =	 "13--22",
  year =	 2006,
  address =	 "Portland, Oregon",
  month =	 sep,
  publisher =	 "{ACM} Press"
}


Functional Hybrid Modeling from an Object-Oriented Perspective

The modeling and simulation of physical systems is of key importance in many areas of science and engineering, and thus can benefit from high-quality software tools. In previous research we have demonstrated how functional programming can form the basis of an expressive language for causal hybrid modeling and simulation. There is a growing realization, however, that a move toward non-causal modeling is necessary for coping with the ever increasing size and complexity of modeling problems. Our goal is to combine the strengths of functional program ming and non-causal modeling to create a powerful, strongly typed fully declarative modeling language that provides modeling and simulation capabilities beyond the current state of the art: in particular, support for highly structurally dynamic systems. Additionally, we think our approach could serve as a semantical framework for studying modeling and simulation languages supporting structural dynamism, and maybe even as a core language in systems where the surface syntax is more conven tional. Although our work is still in its very early stages, we believe that this paper clearly articulates the need for improved modeling languages and shows how functional programming techniques can play a pivotal role in meeting this need.

@Article{Nilsson2007c,
  author =       "Henrik Nilsson and John Peterson and Paul Hudak",
  title =        "Functional Hybrid Modeling from an Object-Oriented
                  Perspective",
  journal =      "Simulation News Europe",
  year =         2007,
  volume =       17,
  number =       2,
  pages =        "29--38",
  month =        sep,
  annote =       "ISSN 0929-2268"
}


Trends in Functional Programming Volume 7

This is Volume 7 of Trends in Functional Programming (TFP). It contains a refereed selection of the papers that were presented at TFP 2006: the Seventh Symposium on Trends in Functional Programming. which took place in Nottingham, 19-21 April, 2006.

TFP is an international forum for researchers from all functional programming communities spanning the entire width of topics in the field. Its goal is to provide a broad view of current and future trends in functional programming in a lively and friendly setting, thus promoting new research directions related to the field of functional programming and the relationship between functional programming and other fields of computer science.

True to the spirit of TFP, the selection of papers in this volume covers a wide range of topics, including dependently typed programming, generic programming, purely functional data structures, function synthesis, declarative debugging, implementation of functional programming languages, and memory management. A particular emerging trend is that of dependently typed programming, reflected by a number of papers in the present selection and by the co-location of TFP and Types 2006.

@Proceedings{Nilsson2007b,
  title = 	 "Trends in Functional Programming Volume 7",
  year = 	 2007,
  editor =	 "Henrik Nilsson",
  publisher =	 "Intellect",
  annote =	 "ISBN: 9781841501888"
}


Switched-On Yampa: Declarative Programming of Modular Synthesizers

In this paper, 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, purely declarative construction of hybrid systems. Since music is a hybrid continuous-time and discrete-time phenomenon, Yampa is a good fit for such applications, offering some unique possibilities compared to most languages targeting music or audio applications. Through the presentation of our synthesizer application, we demonstrate this point and provide insight into the Yampa approach to programming reactive, hybrid systems. We develop the synthesizer gradually, starting with fundamental synthesizer components and ending with an application that is capable of rendering a standard MIDI file as audio with respectable performance.

@InProceedings{Giorgidze2008,
  author = 	 "George Giorgidze and Henrik Nilsson",
  title = 	 "Switched-On {Y}ampa: Declarative Programming of Modular
                  Synthesizers",
  booktitle = 	 "Practical Aspects of Declarative Languages (PADL) 2008",
  pages =	 "282--298",
  year =	 2008,
  editor =	 "Paul Hudak and David S. Warren",
  volume =	 4902,
  series =	 "Lecture Notes in Computer Science",
  address =	 "San Francisco, CA, USA",
  month =	 jan,
  publisher =	 "Springer-Verlag"
}


Type-Based Structural Analysis for Modular Systems of Equations

This paper investigates a novel approach to a type system for modular systems of equations; i.e., equation systems constructed by composition of individual equation system fragments. The purpose of the type system is to ensure, to the extent possible, that the composed system is solvable. The central idea is to attribute a structural type to equation system fragments that reflects which variables occur in which equations. In many instances, this allows over- and underdetermined system fragments to be identified separately, without first having to assemble all fragments into a complete system of equations. The setting of the paper is equation-based, non-causal modelling, specifically Functional Hybrid Modelling (FHM). However, the central ideas are not tied to FHM, but should be applicable to equation-based modelling languages in general, like Modelica, as well as to applications featuring modular systems of equations outside the field of modelling and simulation.

@Article{Nilsson2009,
  author = 	 "Henrik Nilsson",
  title = 	 "Type-Based Structural Analysis for Modular Systems of
		  Equations",
  journal = 	 "Simulation News Europe",
  year = 	 2009,
  volume =	 19,
  number =	 1,
  pages =	 "17--28",
  month =	 apr,
  annote =	 "ISSN 0929-2268"
}


Optimisation of Dynamic, Hybrid Signal Function Networks

Functional Reactive Programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both continuous-time and discrete-time signals (hybrid systems). What sets FRP apart from most other languages for similar applications is its support for systems with dynamic structure and for higher-order data-flow constructs. This raises a range of implementation challenges. This paper contributes towards advancing the state of the art of FRP implementation by studying the notion of signal change and change propagation in a setting of hybrid signal function networks with dynamic structure. To sidestep some problems of certain previous FRP implementations that are structured using arrows, we suggest working with a notion of composable, multi-input and multi-output signal functions. A clear conceptual distinction is also made between continuous-time and discrete-time signals. We then show how establishing change-related properties of the signal functions in a network allows such networks to be simplified (static optimisation) and can help reducing the amount of computation needed for executing the networks (dynamic optimisation). Interestingly, distinguishing between continuous-time and discrete-time signals allows us to characterise the change-related properties of signal functions more precisely than what we otherwise would have been able to, which is helpful for optimisation.

@InProceedings{Sculthorpe2009a,
  author = 	 "Neil Sculthorpe and Henrik Nilsson", 
  title = 	 "Optimisation of Dynamic, Hybrid Signal Function Networks",
  booktitle = 	 "{T}rends in {F}unctional {P}rogramming Volume 9 ({TFP'08})",
  pages =        "97--112",
  year =	 2009,
  editor =	 "Marco Moraz{\'{a}}n and Pieter Koopman and Peter Achten",
  publisher =	 "Intellect"
}


Embedding a Functional Hybrid Modelling Language in Haskell

In this paper we present the first investigation into the implementation of a Functional Hybrid Modelling language for non-causal modelling and simulation of physical systems. In particular, we present a simple way to handle connect constructs: a facility for composing model fragments present in some form in most non-causal modelling languages. Our implementation is realised as a domain-specific language embedded in Haskell. The method of embedding employs quasiquoting, thus demonstrating the effectiveness of this approach for languages that are not suitable for embedding in more traditional ways. Our implementation is available on-line, and thus the first publicly available prototype implementation of a Functional Hybrid Modelling language.

@InProceedings{Giorgidze2011b,
  author = 	 "George Giorgidze and Henrik Nilsson", 
  title = 	 "Embedding a Functional Hybrid Modelling Language in
                  {H}askell",
  booktitle = 	 "Implementation and Application of Functional Languages:
                  20th International Symposium, {IFL} 2008,
                  Revised Selected Papers",
  pages =        "138--155",
  year =	 2011,
  editor =       "Sven-Bodo Scholz and Olaf Chitil",
  volume =       "5836",
  series =       "Lecture Notes in Computer Science",
  publisher =    "Springer-Verlag",
  isbn =         "978-3-642-24451-3",
  doi =          "978-3-642-24451-3"
}


New eyes on visual habituation in locust: an experiment description language for integrative neuroscience.

Neuroscientists have a vast array of instruments at their disposal to examine the function of neural tissue. For example, to investigate visuomotor integration, one can combine in vivo intracellular voltage recordings with visual presentations, focal stimulation of nerves and behavioural observation. While this technological diversity holds enormous promise, it introduces its own set of complexities: how does one control these instruments and ensure that they are configured to perform the experiments most likely to shed light on the hypothesis under consideration? We have developed a domain-specific programming language for describing experiments in cellular and sensory neuroscience. This language aims to let scientists with little programming experience focus on creating a specification of what should be done in an experiment and in the subsequent analyses. We can build complex experiments by combining elementary tasks including animations, sounds, extracellular or intracellular recordings and injection of somatic current waveforms. We have written a series of computer programs to execute these experiments on living animals, or on simulated networks of neurons. These programs allow us to directly compare models and experiments by automatically running the same protocol in vivo and in silico. The results of these trials are stored in a relational database together with the experiment description, information about the animal, and any other available metadata, and are retrieved with a simple custom-built query language.

We have used this new way of conducting experiments to reexamine the response of the descending contralateral movement detector (DCMD) in the locust to looming visual stimuli. The locust is a well- established experimental preparation which permits the study of cross-modal sensorimotor integration. We have measured the kinetics of habituation in the DCMD firing rate response to repeated presentations of similar looming stimuli, and the dependence of this time course on the stimulus amplitude. We have also investigated the influence of auditory stimuli on the visual looming response and the timecourse of its habituation. Finally, we aim to investigate the effect of manipulations of the looming object visual presentation, such as priming portions of the visual field, on the DCMD response. These experiments show how complex multi-modal protocols can be simply defined in an experiment description language and can reliably be carried out repeatedly in a living animal.

@Misc{Nielsen2009,
  author =	 "Nielsen, Thomas A. and Nilsson, Henrik and Matheson, Tom",
  title =	 "New eyes on visual habituation in locust: an experiment
                  description language for integrative neuroscience",
  howpublished = "Poster T14-7C presented at G{\"o}ttingen Meeting of the
                  German Neuroscience Society",
  month =	 mar,
  year =	 2009
}


Braincurry: A domain-specific language for integrative neuroscience

This paper describes Braincurry, a domain-specific, declarative language for describing and analysing experiments in neuroscience. Braincurry has three goals: to allow experiments and data analysis to be described in a way that is sufficiently abstract to serve as a definition; to facilitate carrying out experiments by executing such descriptions; and to be directly usable by end users: neuroscientists. We adopted an experimental and incremental approach to the design and implementation of Braincurry, focusing on the neurophysiological response to visual stimuli in locusts as a test case. Braincurry is currently implemented as an embedding in Haskell, which is a highly effective tool for this kind of exploratory language design. The declarative nature of Haskell and its flexible syntax fitted with our goals. We discuss the requirements for a realistic language meeting the above goals, describe the current Braincurry design and how it may be generalised, and explain how some particularly challenging hard real-time requirements were met.

@InProceedings{Nielsen2010b,
  author = 	 "Nielsen, Thomas A. and Matheson, Tom and Nilsson, Henrik",
  title = 	 "{B}raincurry: A domain-specific language for integrative
                  neuroscience",
  booktitle = 	 "Trends in Functional Programming Volume 10 ({TFP 2009},
                  Revised Selected Papers)",
  year =	 2010,
  editor =       "Horv{\'{a}}th, Zolt{\'{a}}n and Zs{\'{o}}k, Vikt{\'{o}}ria
                  and Koopman, Pieter",
  pages =        "161--176",
  month =	 sep,
  publisher =	 "Intellect",
  isbn =         "978-18-41-50405-6"
}


Higher-Order Non-Causal Modelling and Simulation of Structurally Dynamic Systems

This paper explores a novel approach to the implementation of non-causal modelling and simulation languages supporting highly structurally dynamic systems. One reason the support for structural dynamics is limited in present mainstream non-causal modelling and simulation languages is that they are designed and implemented on the assumption that symbolic processing of models and ultimately compilation of simulation code takes place prior to simulation. We seek to lift that restriction, without sacrificing efficiency, by exploiting just-in-time (JIT) compilation to allow new simulation code, reflecting structural changes, to be generated as the simulation progresses. Our work is carried out in a framework called Functional Hybrid Modelling that supports higher-order modelling, as higher-order modelling lends itself naturally to expressing structural dynamism. However, the central ideas of the paper should be of general interest in the area of structural dynamism. The paper provides an in-depth description of the implementation techniques we have developed as well as a performance evaluation.

@InProceedings{Giorgidze2009b,
  author = 	 "George Giorgidze and Henrik Nilsson",
  title = 	 "Higher-Order Non-Causal Modelling and Simulation of
                  Structurally Dynamic Systems",
  booktitle = 	 "Proceedings of the 7th International {M}odelica
                  {C}onference",
  pages =        "208--218",
  year =	 2009,
  series =	 "Link{\"o}ping Electronic Conference Proceedings",
  address =	 "Como, Italy",
  month =	 sep,
  publisher =	 "Link{\"o}ping University Electronic Press"
}


Safe Functional Reactive Programming through Dependent Types

Functional Reactive Programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both continuous-time and discrete-time signals (hybrid systems). What sets FRP apart from most other languages for similar applications is its support for systems with dynamic structure and for higher-order reactive constructs. Statically guaranteeing correctness properties of programs is an attractive proposition. This is true in particular for typical application domains for reactive programming such as embedded systems. To that end, many existing reactive languages have type systems or other static checks that guarantee domain-specific properties, such as feedback loops always being well-formed. However, they are limited in their capabilities to support dynamism and higher-order data-flow compared with FRP. Thus, the onus of ensuring such properties of FRP programs has so far been on the programmer as established static techniques do not suffice. In this paper, we show how dependent types allow this concern to be addressed. We present an implementation of FRP embedded in the dependently-typed language Agda, leveraging the type system of the host language to craft a domain-specific (dependent) type system for FRP. The implementation constitutes a discrete, operational semantics of FRP, and as it passes the Agda type, coverage, and termination checks, we know the operational semantics is total, which means our type system is safe.

@InProceedings{Sculthorpe2009b,
  author = 	 "Neil Sculthorpe and Henrik Nilsson",
  title = 	 "Safe Functional Reactive Programming through Dependent
                  Types",
  booktitle = 	 "Proceedings of the Fourteenth {ACM} {SIGPLAN} International
                  Conference on Functional Programming (ICFP'09)",
  pages =	 "23--34",
  year =	 2009,
  address =	 "Edinburgh, Scotland",
  month =	 sep,
  publisher =	 "{ACM} Press"
}


Mixed-level Embedding and JIT Compilation for an Iteratively Staged DSL

This paper explores how to implement an iteratively staged domain-specific language (DSL) by embedding into a functional language. The domain is modelling and simulation of physical systems where models are expressed in terms of non-causal differential-algebraic equations; i.e., sets of constraints solved through numerical simulation. What sets our language apart is that the equational constraints are first class entities allowing for an evolving model structure characterised by repeated generation of updated constraints. Hence iteratively staged. Our DSL can thus be seen as a combined functional and constraint programming language, albeit a two-level one, with the functional language chiefly serving as a meta language. However, the two levels do interact throughout the simulation. The embedding strategy we pursue is a mixture of deep and shallow, with the deep embedding enabling just-in-time (JIT) compilation of the constraints as they are generated for efficiency, while the shallow embedding is used for the remainder for maximum leverage of the host language. The paper is organised around a specific DSL, but our implementation strategy should be applicable for iteratively staged languages in general. Our DSL itself is further a novel variation of a declarative constraint programming language.

@InProceedings{Giorgidze2011a,
  author = 	 "George Giorgidze and Henrik Nilsson",
  title = 	 "Mixed-level Embedding and {JIT} Compilation for an
                  Iteratively Staged {DSL}",
  booktitle = 	 "Proceedings of the 19th {W}orkshop on {F}unctional and
                  (Constraint) {L}ogic {P}rogramming ({WFLP 2010})",
  pages =        "48--65",
  year =	 2011,
  editor =	 "Mari\~{n}o, Julio",
  volume =       "6559",
  series =       Lecture Notes in Computer Science,
  publisher =	 Springer-Verlag
}


A functional calculus of physiological evidence (poster)

Thomas A Nielsen(1,2), Henrik Nilsson(2), Tom Matheson(1)

How should we best describe neuroscience experiments and simulations in order for them to be executed, analysed and communicated effectively? Currently, there are two options: as a configuration file for some generic experimental system, or as a program expressed in a conventional programming language. Configuration files tend to be easy to write and read, but are inflexible and only allow a narrow scope of experiments. Programs in conventional languages, on the other hand, are flexible, but hard to write and even harder to understand, thus making them a very poor fit for communicating the ideas of experiments and for formally reason about them. Here, we show that functional reactive programming offers a powerful formalism for neurophysiological experimentation: first, its concepts of signals and events are flexible enough to represent many physiological observations. Second, functions, signals and events are first-class entities allowing a high level of abstraction. For instance, signal transformers and event detectors can be composed within the language from higher-order functions. Third, by focusing on equations and eschewing side effects such as variable mutation and state, FRP is declarative, i.e. expressed in terms of what the essential idea of the experiment is as opposed to the mechanical details of how to carry out the experiment. This makes the descriptions much easier to understand, thus making them an effective tool for communicating experimental setups, and facilitates analysis. We demonstrate how signals, events and durations allow us to structure an experiment on visually evoked spike recordings from insects. We analyse these data with a hierarchical Bayesian model that uses all the recorded spikes rather than relying on point estimators such as averaging or histogram binning of spike times. Since temporal durations can be nested, the hierarchical models can be directly defined in terms of the reactive types we have introduced.

@Misc{Nielsen2010a,
  author =	 "Nielsen, Thomas A. and Nilsson, Henrik and Matheson, Tom",
  title =	 "A functional calculus of physiological evidence",
  howpublished = "Poster presented at the International Neuroinformatics
                  Coordinating Facility (INCF) UK Node Congress, Edinburgh,
                  February 1 - 3, 2010",
  month =	 feb,
  year =	 2010
}


Journal of Functional Programming: Special Issue Dedicated to ICFP 2008

The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP) was held in Victoria, British Columbia, Canada, in September 2008. Peter Thiemann chaired the program committee. After the conference, the authors of a selection of the presented papers were invited to submit extended versions of their work for this special issue of Journal of Functional Programming dedicated to ICFP 2008. All submitted papers were reviewed by at least three referees, including at least one expert, following the standard JFP procedures. In the end, four papers were accepted. These cover a broad range of topics and, taken together, we think they represent well the scope of ICFP 2008.

@Proceedings{Thiemann2010,
  editor =       "Peter Thiemann and Henrik Nilsson",
  year =         2010,
  month =        nov,
  title =        "Journal of Functional Programming: Special Issue Dedicated 
                  to ICFP 2008",
  volume =       "20(5--6)"
}


Static balance checking for first-class modular systems of equations

Characterising a problem in terms of a system of equations is common to many branches of science and engineering. Due to their size, such systems are often described in a modular fashion by composition of individual equation system fragments. Checking the balance between the number of variables (unknowns) and equations is a common approach to early detection of mistakes that might render such a system unsolvable. However, current approaches to modular balance checking have a number of limitations. This paper investigates a more flexible approach that in particular makes it possible to treat equation system fragments as true first-class entities. The central idea is to record balance information in the type of an equation fragment. This information can then be used to determine if individual fragments are well formed, and if composing fragments preserves this property. The type system presented in this paper is developed in the context of Functional Hybrid Modelling (FHM). However, the key ideas are in no way specific to FHM, but should be applicable to any language featuring a notion of modular systems of equations.

@InProceedings{Capper2011,
  author = 	 "John Joseph Capper and Henrik Nilsson",
  title = 	 "Static Balance Checking for First-Class Modular Systems of
                  Equations",
  booktitle = 	 "Trends in Functional Programming: 11th International
                  Symposium, TFP 2010, Norman, OK, USA, May 2010, 
                  Revised Selected Papers",
  editor =       "Rex Page and Zolt{\'{a}}n Horv{\'{a}}th
                  and Vikt{\'{o}}ria Zs{\'{o}}k",
  pages =	 "50--65",
  year =	 2011,
  volume =	 6546,
  series =	 "Lecture Notes in Computer Science,
  publisher =	 "Springer-Verlag",
  isbn =         "Print: 978-3-642-22940-4; Online: 978-3-642-22941-1",
  doi =          "10.1007/978-3-642-22941-1_4"
}


Exploiting structural dynamism in Functional Hybrid Modelling for simulation of ideal diodes

Current main-stream non-casual modelling and simulation languages, like Modelica, are designed and implemented on the assumption that model causality remains fixed during simulation. This simplifies the language design and facilitates the generation of efficient simulation code. In particular, simulation code can be generated once and for all, at compile time. However, for hybrid models, the assumption of fixed causality is very limiting: there are many examples, including simple ones, that cannot be simulated. A half-wave rectifier with an ideal diode and an in-line inductor is one such example. Functional Hybrid Modelling is a new approach to non-causal modelling where models are first-class entities and structural dynamism is supported by switching among model configurations. Fixed causality is thus \emph{not} assumed. Continuous simulation remains efficient thanks to just-in-time generation of simulation code at structural changes and the use of a standard, industrial-strength solver. Re-generation of code at each structural change of course incurs an overhead, but this is typically modest. In this paper we demonstrate how Functional Hybrid Modelling makes it possible to simulate electrical circuits with ideal diodes in a straightforward manner. We consider both a half-wave rectifier and a significantly more challenging full-wave rectifier.

@InProceedings{Nilsson2010,
  author = 	 "Henrik Nilsson and George Giorgidze",
  title = 	 "Exploiting Structural Dynamism in {F}unctional {H}ybrid
                  {M}odelling for Simulation of Ideal Diodes",
  booktitle = 	 "Proceedings of the 7th EUROSIM Congress on Modelling and
                  Simulation",
  year =	 2010,
  address =	 "Prague, Czech Republic",
  month =	 sep,
  publisher =	 "Czech Technical University Publishing House",
  isbn =	 "978-80-01-04589-3"
}


Keeping calm in the face of change: Towards optimisation of FRP by reasoning about change

Functional Reactive Programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals (time-varying values). FRP is based on the synchronous data-flow paradigm and supports both (an approximation to) continuous-time and discrete-time signals (hybrid systems).What sets FRP apart from most other languages for similar applications is its support for systems with dynamic structure and for higher-order reactive constructs.

This paper contributes towards advancing the state of the art of FRP implementation by studying the notion of signal change and change propagation in a setting of structurally dynamic networks of n-ary signal functions operating on mixed continuous-time and discretetime signals. We first define an ideal denotational semantics (time is truly continuous) for this kind of FRP, along with temporal properties, expressed in temporal logic, of signals and signal functions pertaining to change and change propagation. Using this framework, we then show how to reason about change; specifically, we identify and justify a number of possible optimisations, such as avoiding recomputation of unchanging values. Note that due to structural dynamism, and the fact that the output of a signal function may change because time is passing even if the input is unchanging, the problem is significantly more complex than standard change propagation in networks with static structure.

@Article{Sculthorpe2011b,
  author = 	 "Neil Sculthorpe and Henrik Nilsson",
  title = 	 "Keeping Calm in the Face of Change: Towards Optimisation of
		  {FRP} by Reasoning about Change",
  journal = 	 "Journal of Higher-Order and Symbolic Computation",
  year = 	 2011,
  volume =	 23,
  number =	 2,
  pages =	 "227--271",
  issn =         "Print: 1388-3690; Electronic:1573-0557",
  doi =          "10.1007/s10990-011-9068-x"
}


Towards a formal semantics for a structurally dynamic noncausal modelling language

Modelling and simulation languages are evolving rapidly to support modelling of systems of ever increasing size and complexity. A relatively recent development in the area of physical modelling is the noncausal modelling languages. They support a declarative, highly modular modelling approach, promoting the reuse of components. Modelica is a prime example of this class of languages. However, the mainstream representatives of this class of languages provide limited support for higher-order modelling and structurally dynamic systems. Moreover, the semantics of this class of languages remains a relatively unexplored area. Functional Hybrid Modelling (FHM) is a novel approach to noncausal, hybrid modelling that aims to address these concerns. In this paper, we give a semantics to the discrete part of a simple FHM language expressed in dependent type theory. We use Normalisation by Evaluation to produce a type-preserving and terminating normalisation procedure, the latter property being particularly important for FHM as highly structurally dynamic systems are supported by computing new system configurations during simulation. Furthermore, our implementation has been carefully structured to allow continuous aspects of the semantics to be described separately, in whatever way is deemed appropriate, while retaining the ability to describe precisely how a system evolves in response to discrete events.

@InProceedings{Capper2012,
  author = 	 "John Joseph Capper and Henrik Nilsson",
  title = 	 "Towards a Formal Semantics for a Structurally Dynamic
                  Noncausal Modelling Language",
  booktitle = 	 "Types in Language Design and Implementation",
  pages =	 "39--50",
  year =	 2012,
  address =	 "Philadelphia, PA, USA",
  month =	 jan,
  publisher =	 "{ACM} Press",
  isbn =         "978-1-4503-1120-5",
  doi =          "10.1145/2103786.2103792"
}


A formal mathematical framework for physiological observations, experiments and analyses

Experiments can be complex and produce large volumes of heterogeneous data, which make their execution, analysis, independent replication and meta-analysis difficult. We propose a mathematical model for experimentation and analysis in physiology that addresses these problems. We show that experiments can be composed from time-dependent quantities, and be expressed as purely mathematical equations. Our structure for representing physiological observations can carry information of any type and therefore provides a precise ontology for a wide range of observations. Our framework is concise, allowing entire experiments to be defined unambiguously in a few equations. In order to demonstrate that our approach can be implemented, we show the equations that we have used to run and analyse two non-trivial experiments describing visually stimulated neuronal responses and dynamic clamp of vertebrate neurons. Our ideas could provide a theoretical basis for developing new standards of data acquisition, analysis and communication in neurophysiology.

@Article{Nielsen2012,
  author = 	 "Nielsen, Thomas A. and Nilsson, Henrik and Matheson, Tom",
  title = 	 "A formal mathematical framework for physiological
                  observations, experiments and analyses",
  journal = 	 "Journal of The Royal Society Interface",
  year = 	 2012,
  volume =	 9,
  number =	 70,
  pages =	 "1040--1050",
  month =	 may,
  doi =          "10.1098/rsif.2011.0616"
}


Haskell gets argumentative

Argumentation theory is an interdisciplinary field studying how conclusions can be reached through logical reasoning. The notion of argument is completely general, including for example legal arguments, scientific arguments, and political arguments. Computational argumentation theory is studied in the context of artificial intelligence, and a number of computational argumentation frameworks have been put forward to date. However, there is a lack of concrete, high level realisations of these frameworks, which hampers research and applications at a number of levels. We hypothesise that the lack of suitable domain-specific languages in which to formalise argumentation frameworks is a contributing factor. In this paper, we present a formalisation of a particular computational argumentation framework, Carneades, as a case study with a view to investigate the extent to which functional languages are useful as a means to realising computational argumentation frameworks and reason about them.

@Inproceedings{Gijzel2012a,
  author =       "{\noopsort{Gijzel}}van Gijzel, Bas and Nilsson, Henrik",
  title =        "{H}askell Gets Argumentative",
  booktitle =    "Trends in Functional Programming: 13th International
                  Symposium, TFP 2012, St Andrews, UK, June 2012, Revised
                  Selected Papers",
  year  =        2012,
  series =       lncs,
  publisher =    sv,
  note =	 "To appear"
}


Last updated 5 February 2013.