enter search term and/or author name
A type system for certified binaries
Zhong Shao, Valery Trifonov, Bratin Saha, Nikolaos Papaspyrou
A certified binary is a value together with a proof that the value satisfies a given specification. Existing compilers that generate certified code have focused on simple memory and control-flow safety rather than more advanced properties. In...
Regular expression types for XML
Haruo Hosoya, Jérôme Vouillon, Benjamin C. Pierce
We propose regular expression types as a foundation for statically typed XML processing languages. Regular expression types, like most schema languages for XML, introduce regular expression notations such as repetition (*), alternation...
Optimizing aggregate array computations in loops
Yanhong A. Liu, Scott D. Stoller, Ning Li, Tom Rothamel
An aggregate array computation is a loop that computes accumulated quantities over array elements. Such computations are common in programs that use arrays, and the array elements involved in such computations often overlap, especially across...
Automatic discovery of covariant read-only fields
Jens Palsberg, Tian Zhao, Trevor Jim
Read-only fields are useful in object calculi, pi calculi, and statically typed intermediate languages because they admit covariant subtyping, unlike updateable fields. For example, Glew's translation of classes and objects to an intermediate...
Pretty printing with lazy dequeues
There are several purely functional libraries for converting tree structured data into indented text, but they all make use of some backtracking. Over twenty years ago, Oppen published a more efficient imperative implementation of a pretty printer....