ABSTRACT.  

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

ABSTRACT. please, see uploaded PDF file