Holger Stadel Borum will present his work on a visual notation and programming environment for depend types. Detailed information below.
Holger Stadel Borum, PhD Fellow.
A Visual Notation and Programming Environment for Dependent Types
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.