The Dependent Object Type (DOT) calculus was designed to put Scala on a
sound basis, but while DOT relies on structural subtyping, Scala is a
fundamentally class-based language. This impedance mismatch means that a proof
of DOT soundness by itself is ...
We study the basic problem of assigning memoryless workers to tasks with dynamically changing demands. Given a set of w workers and a multiset T ⊆ [t] of |T| = w tasks, a memoryless worker-task assignment function is any function ϕ that assigns the workers ...
Schloss Dagstuhl -- Leibniz-Zentrum fur Informatik2022
Majority-inverter graphs (MIGs) are a logic representation with remarkable algebraic and Boolean properties that enable efficient logic optimizations beyond the capabilities of traditional logic representations. Further, since many nano-emerging technologi ...
Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because d ...
Values need to be represented differently when interacting with certain language features. For example, an integer has to take an object-based representation when interacting with erased generics, although, for performance reasons, the stack-based value re ...
Boolean Algebra with Presburger Arithmetic (BAPA) is a decidable logic that can express constraints on sets of elements and their cardinalities. Problems from verification of complex properties of software often contain fragments that belong to quantifier- ...
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011
To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate multiple user-defined functions, and compare multiple invocations of a function for different arguments. We present decision ...
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2011
Motivated by applications in software verification, we explore automated reasoning about the non-disjoint combination of theories of infinitely many finite structures, where the theories share set variables and set operations. We prove a combination theore ...
Pattern matching is a programming language construct considered essential in functional programming. Its purpose is to inspect and decompose data. Instead, object-oriented programming languages do not have a dedicated construct for this purpose. A possible ...
