Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...
While theoretical and empirical insights suggest that the capacity to represent and process complex syntax is crucial in language as well as other domains, it is still unclear whether specific parsing mechanisms are also shared across domains. Focusing on ...
MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bi ...
Designing digital circuits well is notoriously difficult. This difficulty stems in part from the very
many degrees of freedom inherent in circuit design, typically coupled with the need to satisfy
various constraints. In this thesis, we demonstrate how for ...
The inception of object-oriented programming introduces a category of bugs related to object construction: initialization errors. Every newly created object goes through several initialization states: starting from a state where all fields are uninitialize ...
Quasiquotes have been shown to greatly simplify the task of metaprogramming. This is in part because they hide the data structures of the intermediate representation (IR), instead allowing metaprogrammers to use the concrete syntax of the language they man ...
RDF and SPARQL are established standards for data interchange and querying on the Web. While they have been shown to be useful and applicable in many scenarios, they are not sufficiently adequate for dealing with streams of data and their intrinsic continu ...
