Beluga: programming with dependent types and higher-order data

about them using a simple, powerful technique, called higher-order
abstract syntax (HOAS). Recently, it has been for example successfully
used to specify and verify guarantees about the run-time behavior of
mobile code. However, incorporating logical framework technology into
functional programming to directly allow programmers to describe and
reason about properties of programs from within the programming
language itself has been a major challenge.

In this talk, I will present Beluga, a dependently-typed functional
language which supports programming with data specified in the logical
framework LF. First, I will show how to implement normalization for typed
lambda-terms in Beluga, and highlight its theoretical foundation
based on contextual types. Second, I will discuss practical challenges
regarding type reconstruction for dependently typed systems and
summarize the status of our implementation.