To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 16/10/09 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Vendredi 16 octobre, 10h30 ---------------- Brigitte Pientka ---------------- McGill University ============================================================== Beluga: programming with dependent types and higher-order data ============================================================== The logical framework LF supports specifying formal systems and proofs 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.