View: session overviewtalk overviewside by side with other conferences

09:00-10:15 Session 23G: Invited Talk
Location: FH, Seminarraum 325/1
SPEAKER: Alan Jeffrey


Functional Reactive Programming (FRP) is a style of reactive programming whose semantics is given as time-indexed streams of values. Linear-time Temporal Logic (LTL) is a logic indexed by time, with modalities such as "at all times in the future". In this talk, I will discuss the use of constructive LTL as a type system for FRP, and show that functional reactive programs can serve two purposes: as executable programs, and as proof terms fur constructive LTL. This style of programming has been implemented in Agda, compiled to JavaScript, and linked against the DOM API for Graphical User Interfaces (GUIs). The result is a programming environment which combines interactive code with proofs of tautologies in temporal logic.

10:15-10:45Coffee Break
10:45-13:00 Session 26S: Contributed Talks
Location: FH, Seminarraum 325/1
Terminal semantics for codata types in intensional Martin-Löf type theory
SPEAKER: unknown

ABSTRACT. In this work, we study the notions of relative comonad and comodule over a relative comonad, and use these notions to give a terminal coalgebra semantics for the coinductive type families of streams and of infinite triangular matrices, respectively, in intensional Martin-Löf type theory. Our results are mechanized in the proof assistant Coq.

A Unifying Framework for Primitive Ontological Relations in Dependent Type Theory
SPEAKER: unknown

ABSTRACT. In the development of foundational ontologies, a challenging problem which has not yet received a satisfying solution is the logical co-existence of part-whole relations and subsumption within a single framework. In this paper, we will explain how dependent type theory, and more precisely the Calculus of Inductive Constructions based on intuitionistic logic has a sufficient power for representing and reasoning coherently with these two relations.

Domain Specific Languages of Mathematics
SPEAKER: unknown

ABSTRACT. We present a small number of examples of using the computer science perspective to the teaching of continuous mathematics by focusing on the domain-specific languages underlying the mathematical areas.

Relational ornaments
SPEAKER: unknown

ABSTRACT. We propose a relational reformulation of McBride’s ornaments, which leads to new constructions that are not possible with the original formulation.

13:00-14:30Lunch Break
14:30-16:00 Session 31P: Contributed Talks
Location: FH, Seminarraum 325/1
An Embedded Hardware Description Language using Dependent Types
SPEAKER: unknown

ABSTRACT. We present a Embedded Domain-Specific Language (EDSL) for hardware description using the dependently-typed language Agda as host. Circuits modeled in this EDSL can be simulated, exported to VHDL netlists, and have properties proven about their functional correctness.

Type-Directed Editing for Dependently-Typed Programs.
SPEAKER: unknown

ABSTRACT. Dependent types allow a programmer to state sophisticated properties of programs. Recent demonstrations suggest that types should be leveraged during programming and editing to direct editing actions and assist the programmer with constructing type correct programs in the first instance.

Toward this end, we are exploring type-directed editing. Type-directed editing proposes to offer programmers a rich set of high-level programming actions which both respect type-correctness of programs and leverage typing information to assist the programmer. Our goal is to give a semantics for editing in which every editing action results in a type-correct program, and to implement these semantics with a well-engineered and friendly user interface. We hypothesize that by removing the search for a typechecking program in the space of text strings from the programming process, we can increase the productivity of programmers.

Tool Demonstration: An IDE for Programming and Proving in Idris
SPEAKER: unknown

ABSTRACT. Dependently typed programming languages have a rich type system, which enables developers to combine proofs with programs, sometimes even eroding the boundary between the activities of proving and programming. This introduces new challenges for integrated development environments that must support this boundary. Instead of reimplementing large parts of a compiler, such as a type checker and a totality checker, we extended the Idris compiler with a structured, machine-readable protocol for interacting with other programs. Furthermore, we developed an IDE for Idris in Emacs, which uses this structured input and output mode, that attempts to combine features from both proof assistant interfaces and rich programming environments such as SLIME. The Idris extension turned out to be generally useful, and has been used in applications such as an IRC bot, an interactive website for trying out Idris, and support for other editors.

16:00-16:30Coffee Break
16:30-18:00 Session 34R: Contributed Talks
Location: FH, Seminarraum 325/1
Scrapping Your Dependently-Typed Boilerplate is Hard

ABSTRACT. More complex programs that model programming languages or specific domain information end up with large nested data structures, and as a consequence changing even simple properties require a full traversal of the structure. The Haskell community has developed various techniques that try to reduce this boilerplate by providing generic frameworks querying and traversal, such as Scrap Your Boilerplate (SYB)[1] and Uniplate [2]. Since many of the modern dependently-typed languages such as Agda[3] or Idris[4] are inspired by Haskell, it would be reasonable to expect that such frameworks could be provided in these languages. However, as I will show in my presentation there are some unresolved issues that prevent these approaches from being used as-is.

On a style of presentation of type systems

ABSTRACT. We outline a way of formulating and explaining type systems/functional programming languages that we believe could be both logically well-founded and didactic. We propose to discuss the details for both simple and dependent type systems.

Sequential decision problems and a computational theory of avoidability
SPEAKER: unknown

ABSTRACT. please, see uploaded PDF file