Sciweavers

Share
FLOPS
2010
Springer

Beluga: Programming with Dependent Types, Contextual Data, and Contexts

11 years 5 months ago
Beluga: Programming with Dependent Types, Contextual Data, and Contexts
The logical framework LF provides an elegant foundation for specifying formal systems and proofs and it is used successfully in a wide range of applications such as certifying code and mechanizing metatheory of programming languages. However, incorporating LF technology into functional programming to allow programmers to specify and reason about formal guarantees of their programs from within the programming language itself has been a major challenge. In this paper, we present an overview of Beluga, a framework for programming and reasoning with formal systems. It supports specifying formal systems in LF and it also provides a dependently typed functional language that supports analyzing and manipulating LF data via pattern matching. A distinct feature of Beluga is its direct support for reasoning with contexts and contextual objects. Taken together these features lead to powerful language which supports writing compact and elegant proofs.
Brigitte Pientka
Added 18 May 2010
Updated 18 May 2010
Type Conference
Year 2010
Where FLOPS
Authors Brigitte Pientka
Comments (0)
books