Dependent types, linear types and operating systems

Add to your list(s) Download to your calendar using vCal

• Matthew Danish (University of Cambridge)
• Thursday 28 April 2016, 13:00-14:00
• FW26.

If you have a question about this talk, please contact Dominic Orchard.

Operating systems software is fundamental to modern computer systems: all other applications are dependent upon the correct and timely provision of basic system services. At the same time, advances in programming languages and type theory have lead to the creation of functional programming languages with type systems that are designed to combine theorem proving with practical systems programming.

This talk will focus on introducing dependent and linear types using the ATS programming language, and in the context of the Terrier operating system that is written using ATS . No prior knowledge of either is assumed.

The Terrier operating system project focuses on low-level systems programming in the context of a multi-core, real-time, embedded system, while taking advantage of a dependently typed programming language named ATS to improve reliability. Terrier is a new point in the design space for an operating system, one that leans heavily on an associated programming language, ATS , to provide safety that has traditionally been in the scope of hardware protection and kernel privilege. Terrier tries to have far fewer abstractions between program and hardware. The purpose of Terrier is to put programs as much in contact with the real hardware, real memory, and real timing constraints as possible, while still retaining the ability to multiplex programs and provide for a reasonable level of safety through static analysis.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Programming Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.