Brigitte Pientka is an Associate Professor in the School of Computer Science at
McGill University, and leading the Computation and Logic group. She received her
PhD from Carnegie Mellon University in 2003, and studied previously at the University
of Edinburgh and Technical University of Darmstadt

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Expert Audience

English

60 Minutes

Saarbrücken

Software systems should be robust, reliable, and predictable. Today, we
routinely reason about the runtime behavior of software using formal
systems such as type systems or logics for access control or information flow to
establish safety and liveness properties.

In this talk, I will survey Beluga, a dependently typed programming and proof
environment. It supports specifying formal systems in the logical framework LF
and directly supports common and tricky routines dealing with variables, such as
capture-avoiding substitution and renaming. Moreover, Beluga allows embedding LF
objects together with their context in programs and types supporting inductive
and coinductive definitions. I will discuss how to write inductive and
coinductive proofs about LF specifications using three different examples: type
uniqueness, normalization by evaluation, and the fact that evaluating a
lambda-term cannot yield a value and diverge at the same time. Taken together
these examples demonstrate the elegance and conciseness of Beluga for
specifying, verifying and validating safety properties.

Brigitta Hansen

0681 93039102

--email hidden

Yes

Kaiserslautern

G26

206

passcode not visible

logged in users only