06/11/2019 – Talk: “A Visual Notation and Programming Environment for Dependent Types” by Holger Stadel Borum

Holger Stadel Borum will present his work on a visual notation and programming environment for depend types. Detailed information below.

SPEAKER

Holger Stadel Borum, PhD Fellow.

TITLE

A Visual Notation and Programming Environment for Dependent Types

ABSTRACT

We present a visual notation and programming environment for a first order functional language with dependent types. In the notation types are represented as shapes, terms are represented as figures, and application is represented as nested shapes/figures. The representation emphasizes a mental model where terms are thought of as real world objects. The notation affords a transparent programming environment with visual step-by-step execution and type checking. The notation is intended as a supplement in the teaching of proof assistants or dependent types.