Difference between revisions of "NL-FP dag 2019"

From Clean
Jump to navigationJump to search
Line 82: Line 82:
 
|Dinner (optional)
 
|Dinner (optional)
 
|}
 
|}
 +
 +
== Talks ==
 +
 +
=== Shubham Yadav: Ball Collision Model — Hardware Designing with Multiple Clock Cycle Components in Cλash ===
 +
Cλash as a functional hardware description language is a slight variation of Haskell, and its compiler transforms high level designs into low level hardware languages, like VHDL and (System) Verilog. This presentation describes some ways to develop hardware designs which include multiple clock cycle components (having both static and dynamic latency) at higher level. To model these multiple clock cycle operations, two different approaches are discussed: dataflow modelling and usage of delayed signals (a newtype defined in the Cλash library).
 +
 +
=== Klara Marntirosian: COCHIS a Calculus with Stable and Coherent Implicits ===
 +
Implicit Progamming (IP) mechanisms infer values by type-directed resolution, making programs more compact and easier to read. Examples of IP mechanisms include Haskell’s type classes, Scala’s implicits, Agda’s instance arguments, Coq’s type classes, and Rust’s traits. The design of IP mechanisms has led to heated debate: proponents of one school argue for the desirability of strong reasoning properties; while proponents of another school argue for the power and flexibility of local scoping or overlapping instances. The current state of affairs seems to indicate that the two goals are at odds with one another and cannot easily be reconciled.
 +
 +
This talk presents COCHIS, the Calculus Of CoHerent ImplicitS, an improved variant of the implicit calculus that offers flexibility while preserving two key properties: coherence and stability of type substitutions. COCHIS supports polymorphism, local scoping, overlapping instances, first-class instances, and higher-order rules, while remaining type safe, coherent and stable under type substitution.
 +
 +
=== Haye Böhm: Asynchronous Shares in a Synchronous World ===
 +
To be announced.
 +
 +
=== Jappie Klooster: Fullstack Haskell with reflex & servant ===
 +
The basics of functional reactive programming are briefly
 +
explained, and how they apply to reflex. Then we see the benefits of
 +
full stack haskell in a live coding session! We'll make a widget or
 +
add/change an endpoint or both depending on time.
 +
 +
=== Wim Bast: Declarative programming using Dclare ===
 +
Dclare is a (open-source) Java library used to develop declarative-language run-times.
 +
Dclare is a reactive en incremental framework optimized for dynamic systems.
 +
It not a pure functional solution because it reacts to, and produces state changes.
 +
However, Dclare 'hides' all imperative aspects from the programmer, similar to real functional languages.
 +
Based on some examples and life-programming Wim Bast wil show the capabilities of this framework.
 +
Dclare is used in some industrie products, under-which the Dutch tax-office..
 +
The goal of this presentation is to discuss language evolution and compare the functional with the declarative paradigm.
 +
 +
=== Gert-Jan Bottu: Proving Haskell's Type Class Resolution Coherent ===
 +
Haskell’s elaboration-based type class resolution is generally
 +
nondeterministic: there can be multiple ways to satisfy a wanted constraint in terms of global instances and locally given constraints.
 +
Coherence is the key property that keeps this sane; it guarantees that, despite the nondeterminism, programs still behave predictably. Even though elaboration-based resolution is generally assumed coherent, this property has never formally been proven.
 +
 +
This talk gives an introduction to Haskell’s dictionary-based type class resolution, explains the need for a coherent elaboration and shows how we managed to successfully solve this age-old problem!
 +
 +
=== Tim Steenvoorden: TopHat: A formal calculus for modular interactive workflows ===
 +
Task-Oriented Programming (TOP) is a programming paradigm that focusses on modelling real world collaborations between people.
 +
It prescribes a declarative programming style to specify multi-user workflows.
 +
Workflows can be higher-order.
 +
They communicate through typed values on a local or global level.
 +
Such specifications can be turned into interactive applications for different platforms,
 +
supporting collaboration during execution.
 +
 +
In this talk we decompose the rich features of TOP into elementary language elements,
 +
which makes them suitable for formal treatment.
 +
We use the simply typed lambda calculus, extended with pairs and references, as a base language.
 +
On top of this language, we develop TopHat, a calculus for modular interactive workflows.
 +
With TopHat we prepare a way to formally reason about TOP systems.
 +
 +
We describe TopHat by means of a layered semantics.
 +
These layers consist of multiple big step evaluations on expressions,
 +
and two labelled transition systems, handling user inputs.
 +
We show some interesting properties of this machinery.
 +
This approach allows for comparison with other work in the field.
 +
We place TopHat in perspective with the process calculus CSP.
 +
 +
=== Dirk Hünniger: From Wikipedia to LaTeX ===
 +
It is often desirable to have access to Wikipedia articles in LaTeX
 +
format. A translation by hand is typically time-consuming and
 +
error-prone. Thus it is natural to look for algorithmic solutions to
 +
thisproblem. Our solution is currently available free of charge under an
 +
open source license for Windows and Debian GNU/Linux. It is not limited
 +
to Wikipedia but supports all servers running the same wiki software
 +
(MediaWiki) as Wikipedia. In particular, it is also possible to process
 +
local wikis available only on private networks inside institutions.
 +
 +
=== Alejandro Serrano Mena: Classes of Arbitrary Kind ===
 +
To be announced.
  
 
== Contact ==
 
== Contact ==

Revision as of 11:56, 7 January 2019

The Dutch Functional Programming Day is an annual gathering of researchers, students, and practitioners sharing a common interest in functional programming. The day features talks that cover the latest advances in research, teaching, and applications in the functional programming area. Coffee and lunch breaks provide ample opportunity for networking with your colleagues and meeting new people. Experts and newcomers to the field are equally welcome.

The NL-FP day 2019 takes place on Friday, January 11, 2019 and will be hosted by the Netherlands Defence Academy.

Location

The NL-FP dag will take place at the "Societeit onder de Toren" at the "Trip van Zoudtlandt Kazerne" in Breda. The adress is: De la Reijweg 95, 4818 BA.

Google Maps

OpenStreetMap

Program

The day will follow the traditional FP-Day format: A diverse mix of presentations with long coffee breaks and time to chat.

Time Speaker Title
10:00 Organization Welcome at the NLDA
10:25 Shubham Yadav Ball Collision Model — Hardware Designing with Multiple Clock Cycle Components in Cλash
10:50 Klara Marntirosian COCHIS a Calculus with Stable and Coherent Implicits
11:15 Coffee Break
11:45 Haye Böhm Asynchronous Shares in a Synchronous World
12:10 Jappie Klooster Fullstack Haskell with reflex & servant
12:35 Lunch
14:00 Wim Bast Declarative programming using Dclare
14:25 Gert-Jan Bottu Proving Haskell's Type Class Resolution Coherent
14:50 Tim Steenvoorden TopHat: A formal calculus for modular interactive workflows
15:15 Coffee break
15:45 Dirk Hünniger From Wikipedia to LaTeX
16:10 Alejandro Serrano Mena Classes of Arbitrary Kind
16:35 Organizers Closing and Announcements
16:45 Drinks
18:00 Dinner (optional)

Talks

Shubham Yadav: Ball Collision Model — Hardware Designing with Multiple Clock Cycle Components in Cλash

Cλash as a functional hardware description language is a slight variation of Haskell, and its compiler transforms high level designs into low level hardware languages, like VHDL and (System) Verilog. This presentation describes some ways to develop hardware designs which include multiple clock cycle components (having both static and dynamic latency) at higher level. To model these multiple clock cycle operations, two different approaches are discussed: dataflow modelling and usage of delayed signals (a newtype defined in the Cλash library).

Klara Marntirosian: COCHIS a Calculus with Stable and Coherent Implicits

Implicit Progamming (IP) mechanisms infer values by type-directed resolution, making programs more compact and easier to read. Examples of IP mechanisms include Haskell’s type classes, Scala’s implicits, Agda’s instance arguments, Coq’s type classes, and Rust’s traits. The design of IP mechanisms has led to heated debate: proponents of one school argue for the desirability of strong reasoning properties; while proponents of another school argue for the power and flexibility of local scoping or overlapping instances. The current state of affairs seems to indicate that the two goals are at odds with one another and cannot easily be reconciled.

This talk presents COCHIS, the Calculus Of CoHerent ImplicitS, an improved variant of the implicit calculus that offers flexibility while preserving two key properties: coherence and stability of type substitutions. COCHIS supports polymorphism, local scoping, overlapping instances, first-class instances, and higher-order rules, while remaining type safe, coherent and stable under type substitution.

Haye Böhm: Asynchronous Shares in a Synchronous World

To be announced.

Jappie Klooster: Fullstack Haskell with reflex & servant

The basics of functional reactive programming are briefly explained, and how they apply to reflex. Then we see the benefits of full stack haskell in a live coding session! We'll make a widget or add/change an endpoint or both depending on time.

Wim Bast: Declarative programming using Dclare

Dclare is a (open-source) Java library used to develop declarative-language run-times. Dclare is a reactive en incremental framework optimized for dynamic systems. It not a pure functional solution because it reacts to, and produces state changes. However, Dclare 'hides' all imperative aspects from the programmer, similar to real functional languages. Based on some examples and life-programming Wim Bast wil show the capabilities of this framework. Dclare is used in some industrie products, under-which the Dutch tax-office.. The goal of this presentation is to discuss language evolution and compare the functional with the declarative paradigm.

Gert-Jan Bottu: Proving Haskell's Type Class Resolution Coherent

Haskell’s elaboration-based type class resolution is generally nondeterministic: there can be multiple ways to satisfy a wanted constraint in terms of global instances and locally given constraints. Coherence is the key property that keeps this sane; it guarantees that, despite the nondeterminism, programs still behave predictably. Even though elaboration-based resolution is generally assumed coherent, this property has never formally been proven.

This talk gives an introduction to Haskell’s dictionary-based type class resolution, explains the need for a coherent elaboration and shows how we managed to successfully solve this age-old problem!

Tim Steenvoorden: TopHat: A formal calculus for modular interactive workflows

Task-Oriented Programming (TOP) is a programming paradigm that focusses on modelling real world collaborations between people. It prescribes a declarative programming style to specify multi-user workflows. Workflows can be higher-order. They communicate through typed values on a local or global level. Such specifications can be turned into interactive applications for different platforms, supporting collaboration during execution.

In this talk we decompose the rich features of TOP into elementary language elements, which makes them suitable for formal treatment. We use the simply typed lambda calculus, extended with pairs and references, as a base language. On top of this language, we develop TopHat, a calculus for modular interactive workflows. With TopHat we prepare a way to formally reason about TOP systems.

We describe TopHat by means of a layered semantics. These layers consist of multiple big step evaluations on expressions, and two labelled transition systems, handling user inputs. We show some interesting properties of this machinery. This approach allows for comparison with other work in the field. We place TopHat in perspective with the process calculus CSP.

Dirk Hünniger: From Wikipedia to LaTeX

It is often desirable to have access to Wikipedia articles in LaTeX format. A translation by hand is typically time-consuming and error-prone. Thus it is natural to look for algorithmic solutions to thisproblem. Our solution is currently available free of charge under an open source license for Windows and Debian GNU/Linux. It is not limited to Wikipedia but supports all servers running the same wiki software (MediaWiki) as Wikipedia. In particular, it is also possible to process local wikis available only on private networks inside institutions.

Alejandro Serrano Mena: Classes of Arbitrary Kind

To be announced.

Contact

  • Bas Lijnse (b.lijnse@cs.ru.nl or b.lijnse@mindef.nl)
  • Jan Martin Jansen (JM.Jansen.04@mindef.nl)

Dinner

The dinner is optional and at your own cost. The dinner will take place at "Tortillas" at the Grote Markt in Breda where we will be served a "Variacion a la Tortillas". For more information see http://www.tortillas.nl.

Registration

Participation is free, but you will need to register. The deadline for registration is Friday January 4, 2019. We need to supply a list of participants to the venue. If you are not registered you won't be allowed in.

To register simply can simply send an e-mail with the following information:

  • Name (will be published in the list of participants)
  • Affiliation (optional)
  • E-mail address (will only be used to inform you about the FP-day)
  • Whether you are planning to join the dinner