Blogs (9) >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Fri 4 Nov 2016 10:55 - 11:20 at Matterhorn 1 - Typing, in Practice Chair(s): Sebastian Erdweg

Existing approaches for detecting type errors in unsafe languages are limited. Static analysis methods are imprecise, and often require source-level changes, while most dynamic methods check only memory properties (bounds, liveness, etc.), owing to a lack of run-time type information. This paper describes libcrunch, a system for binary-compatible run-time type checking of unmodified unsafe code, currently focusing on C. Practical experience shows that our prototype implementation is easily applicable to many real codebases without source-level modification, correctly flags programmer errors with a very low rate of false positives, offers a very low run-time overhead, and covers classes of error caught by no previously existing tool.

I did my Bachelor’s and PhD degrees at the University of Cambridge. My initial research background was in operating systems, hypervisors and the like, with a little networking and distributed systems thrown in. Moving some way up the stack, my PhD work centred on the programmer-facing problem of building software by composition of ill-matched components, for which I developed the Cake language. From January 2011 until March 2012 I was a James Martin Fellow in the Department of Computer Science at the University of Oxford, mostly focused on program analysis and the problem of combining state-space methods (e.g. symbolic execution) with syntactic methods (e.g. type checking). From May 2012 to May 2013, I was a postdoctoral researcher at USI’s Faculty of Informatics in Lugano, Switzerland, working on programmer-facing dynamic analysis infrastructure for Java-like virtual machines. From May until October 2013 I was temporarily a Research Assistant at Oracle Labs, on the Alphabet Soup project, working on native object code and debugging support in the Truffle/SubstrateVM stack. Since 2013 I have been a Research Associate back at the University of Cambridge Computer Laboratory, working on various topics with robustness in low-level programming as a recurring theme. I have also worked (some time ago) for Opal Telecom and ARM, and (more recently) and as a consultant for Ellexus.

Conference Day
Fri 4 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Typing, in PracticeOOPSLA at Matterhorn 1
Chair(s): Sebastian ErdwegDelft University of Technology, Netherlands
A Practical Framework for Type Inference Error Explanation
Calvin LoncaricUniversity of Washington, Satish ChandraSamsung Research America, Manu SridharanSamsung Research America, Cole SchlesingerSamsung Research America
DOI Pre-print Media Attached
Dynamically Diagnosing Type Errors in Unsafe CodeAEC
Stephen KellUniversity of Cambridge
DOI Media Attached
First-Class Effect Reflection for Effect-Guided Programming
Yuheng LongIowa State University, Yu David Liu, Hridesh RajanIowa State University, USA
Java and Scala's Type Systems are Unsound: The Existential Crisis of Null PointersAEC
Nada AminEPFL, Ross TateCornell University
Link to publication DOI Pre-print