Software Defined Networking (SDN) programs are written with respect to assumptions on software and hardware facilities and protocol definitions. Silent mismatches between the expected feature set and implemented feature set of SDN artifacts can easily lead to hard to debug network configurations, decreased network performance, outages, or worse, security vulnerabilities. We show how the paradigm of axiomatic programming, supported by practical dependent types, provides effective support for SDN executable specifications and verification.​

Pattern matching is an abstraction mechanism that can greatly simplify source code. We present functional-style pattern matching for C++ implemented as a library, called Mach71. All the patterns are user-definable, can be stored in variables, passed among functions, and allow the use of class hierarchies. As an example, we implement common patterns used in functional languages.

Incorrect implementations of network protocol message specifications affect the stability, security, and cost of network system development. Most implementation defects fall into one of three categories of well defined message constraints. However, the general process of constructing network protocol stacks and systems does not capture these categorical constraints. We introduce a systems programming language with new abstractions that capture these constraints. Safe and efficient implementations of standard message handling operations are synthesized by our compiler, and whole-program analysis is used to ensure constraints are never violated. We present language examples using the OpenFlow protocol.

Selecting operations based on the run-time type of an object is key to many object-oriented and functional programming techniques. We present a technique for implementing open and efficient type switching on hierarchical extensible data types. The technique is general and copes well with C++ multiple inheritance. To simplify experimentation and gain realistic performance using production-quality compilers and tool chains, we implement a type switch construct as an ISO C++11 library, called Mach7. This library-only implementation provides concise notation and outperforms the visitor design pattern, commonly used for case analysis on types in object-oriented programming. For closed sets of types, its performance roughly equals equivalent code in functional languages, such as OCaml and Haskell. The type-switching code is easier to use and is more expressive than hand-coded visitors are. The library is non-intrusive and circumvents most of the extensibility restrictions typical of the visitor design pattern. It was motivated by applications involving large, typed, abstract syntax trees.

We present a formal operational semantics and its Coq mechanization for the C++ object model, featuring object construction and destruction, shared and repeated multiple inheritance, and virtual function call dispatch. These are key C++ language features for high-level system programming, in particular for predictable and reliable resource management. This paper is the first to present a formal mechanized account of the metatheory of construction and destruction in C++, and applications to popular programming techniques such as "resource acquisition is initialization". We also report on irregularities and apparent contradictions in the ISO C++03 and C++11 standards.

This paper proposes a non-intrusive automatic parallelization framework for typeful and property-aware computer algebra systems. Automatic parallelization remains a promising computer program transformation for exploiting ubiquitous concurrency facilities available in modern computers. The framework uses semantics-based static analysis to extract reductions in library components based on algebraic properties. An early implementation shows up to 5 times speed-up for library functions and homotopy-based polynomial system solver. The general framework is applicable to algebraic computation systems and programming languages with advanced type systems that support user-defined axioms or annotation systems.

Object layout - the concrete in-memory representation of objects - raises many delicate issues in the case of the C++ language, owing in particular to multiple inheritance, C compatibility and separate compilation. This paper formalizes a family of C++ object layout schemes and mechanically proves their correctness against the operational semantics for multiple inheritance of Wasserrab et al. This formalization is flexible enough to account for space-saving techniques such as empty base class optimization and tail-padding optimization. As an application, we obtain the first formal correctness proofs for realistic, optimized object layout algorithms, including one based on the popular "common vendor" Itanium C++ application binary interface. This work provides semantic foundations to discover and justify new layout optimizations; it is also a first step towards the verification of a C++ compiler front-end.

This paper describes the design and implementation of an algorithmic differentiation framework in the Axiom computer algebra system. Our implementation works by transformations on Spad programs at the level of the typed abstract syntax tree -- Spad is the language for extending Axiom with libraries. The framework illustrates an algebraic theory of algorithmic differentiation, here only for Spad programs, but we suggest that the theory is general. In particular, if it is possible to define a compositional semantics for programs, we define the exact requirements for when a program can be algorithmically differentiated. This leads to a general algorithmic differentiation system, and is not confined to functions which compute with basic data types, such as floating point numbers.

Generic programming has emerged as an important technique for the development of highly reusable and efficient software libraries. In C++, generic programming is enabled by the flexibility of templates, the C++ type parametrization mechanism. However, the power of templates comes with a price: generic (template) libraries can be more difficult to use and develop than non-template libraries and their misuse results in notoriously confusing error messages. As currently defined in C++98, templates are unconstrained, and type-checking of templates is performed late in the compilation process, i.e., after the use of a template has been combined with its definition. To improve the support for generic programming in C++, we introduce concepts to express the syntactic and semantic behavior of types and to constrain the type parameters in a C++ template. Using concepts, type-checking of template definitions is separated from their uses, thereby making templates easier to use and easier to compile. These improvements are achieved without limiting the flexibility of templates or decreasing their performance - in fact their expressive power is increased. This paper describes the language extensions supporting concepts, their use in the expression of the C++ Standard Template Library, and their implementation in the ConceptGCC compiler. Concepts are candidates for inclusion in the upcoming revision of the ISO C++ standard, C++0x.

C++ templates are key to the design of current successful mainstream libraries and systems. They are the basis of programming techniques in diverse areas ranging from conventional general-purpose programming to software for safety-critical embedded systems. Current work on improving templates focuses on the notion of concepts (a type system for templates), which promises significantly improved error diagnostics and increased expressive power such as concept-based overloading and function template partial specialization. This paper presents C++ templates with an emphasis on problems related to separate compilation. We consider the problem of how to express concepts in a precise way that is simple enough to be usable by ordinary programmers. In doing so, we expose a few weakness of the current specification of the C++ standard library and suggest a far more precise and complete specification. We also present a systematic way of translating our proposed concept definitions, based on use-patterns rather than function signatures, into constraint sets that can serve as convenient basis for concept checking in a compiler.