BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Dependent types\, linear types and operating systems - Matthew Dan
 ish (University of Cambridge)
DTSTART:20160428T120000Z
DTEND:20160428T130000Z
UID:TALK65778@talks.cam.ac.uk
CONTACT:Dominic Orchard
DESCRIPTION:Operating systems software is fundamental to modern computer\n
 systems: all other applications are dependent upon the correct and\ntimely
  provision of basic system services. At the same time\,\nadvances in progr
 amming languages and type theory have lead to the\ncreation of functional 
 programming languages with type systems that\nare designed to combine theo
 rem proving with practical systems\nprogramming.\n\nThis talk will focus o
 n introducing dependent and linear types using the ATS programming languag
 e\, and in the context of the Terrier operating system that is written usi
 ng ATS. No prior knowledge of either is assumed.\n\nThe Terrier operating 
 system project focuses on\nlow-level systems programming in the context of
  a multi-core\,\nreal-time\, embedded system\, while taking advantage of a
  dependently\ntyped programming language named ATS to improve\nreliability
 . Terrier is a new point in the design space for an\noperating system\, on
 e that leans heavily on an associated\nprogramming language\, ATS\, to pro
 vide safety that has traditionally\nbeen in the scope of hardware protecti
 on and kernel\nprivilege. Terrier tries to have far fewer abstractions bet
 ween\nprogram and hardware. The purpose of Terrier is to put programs as\n
 much in contact with the real hardware\, real memory\, and real timing\nco
 nstraints as possible\, while still retaining the ability to\nmultiplex pr
 ograms and provide for a reasonable level of safety\nthrough static analys
 is.
LOCATION:FW26
END:VEVENT
END:VCALENDAR