Gabriele Keller

Share

Associate Professor in the Computer Science and Engineering Department at UNSW Australia
@gckeller

Gabriele Keller is also a Principal Researcher at Data61 (formerly NICTA) in the Trustworthy Systems project. Her research interest are type systems, functional languages, and how these languages can be used to reduce the costs of software development, in particular in the context of high-performance computing and safety critical systems.

She contributed to the design of type families in Haskell, and is one of the co-authors of the paper ””Associated Type Synonyms”“, which recently won the ACM SIGPLAN Most Influential ICFP Paper Award.

YOW! Lambda Jam 2016 Brisbane

Bringing Down the Cost of Verification

KEYNOTE –  VIEW SLIDES WATCH VIDEO

Producing formally verified software is expensive, as it is a time consuming, often tedious process, which requires expert skills not widely available. If we want to reduce these costs, we need to automate as much of the process as possible, and we need to make the technology more accessible to developers without specialised skills in verification. This talk explores some of the issues of verification, in particular in the context of file systems and presents a language based approach to systems code verification. Using a strict, purely functional language with linear types, and a verifying compiler results in a significant reduction of the costs involved.