Abstract
With the incresasing importance of program verification, an issue that has been receiving more attention is the certification of verification tools, addressing the vernacular question: Who verifies the verifier?. In this paper we approach this meta-verification problem by focusing on a fundamental component of program verifiers: the Verification Conditions Generator (VCGen), responsible for producing a set of proof obligations from a program and a specification. The semantic foundations of VCGens lie in program logics, such as Hoare logic, Dynamic logic, or Separation logic, and related predicate transformers. Dynamic logic is the basis of the KeY system, one of the foremost deductive verifiers, whose logic makes use of the notion of update, which is quite intricate to formalize. In this paper we derive systematically, based on a KeY-style dynamic logic, a correct-by-construction VCGen for a toy programming language. Our workflow covers the entire process, from the logic to the VCGen. It is implemented in the Why3 tool, which is itself a program verifier. We prove the soundness and (an appropriate notion of) completeness of the logic, then define a VCGen for our language and establish its soundness. Dynamic logic is one of a variety of research topics that our dear friend and colleague Luis Soares Barbosa has, over the years, initiated and promoted at the University of Minho. It is a pleasure for us to dedicate this work to him on the occasion of his 60th birthday.

Abstract
Constructor subtyping is a form of subtyping in which an inductive type s is viewed as a subtype of another inductive type t if t has more constructors than s. As suggested in [5,12], its (potential) uses include proof assistants and functional programming languages. In this paper, we introduce and study the properties of a simply typed ?-calculus with record types and datatypes, and which supports record subtyping and constructor subtyping. In the first part of the paper, we show that the calculus is confluent and strongly normalizing. In the second part of the paper, we show that the calculus admits a well-behaved theory of canonical inhabitants, provided one adopts expansive extensionality rules, including ?-expansion, surjective pairing, and a suitable expansion rule for datatypes. Finally, in the third part of the paper, we extend our calculus with unbounded recursion and show that confluence is preserved. © Springer-Verlag Berlin Heidelberg 1999.

Abstract

Abstract
We show that a wide class of bidirectional data-flow analyses and program optimizations based on them admit declarative descriptions in the form of type systems. The salient feature is a clear separation between what constitutes a valid analysis and how the strongest one can be computed (via the type checking versus principal type inference distinction). The approach also facilitates elegant relational semantic soundness definitions and proofs for analyses and optimizations, with an application to mechanical transformation of program proofs, useful in proof-carrying code. Unidirectional forward and backward analyses are covered as special cases; the technicalities in the general bidirectional case arise from more subtle notions of valid and principal types. To demonstrate the viability of the approach we consider two examples that are inherently bidirectional: type inference (seen as a data-flow problem) for a structured language where the type of a variable may change over a program's run and the analysis underlying a stack usage optimization for a stack-based low-level language. ©2009 ACM.

Abstract
Data-flow analyses, such as live variables analysis, available expressions analysis etc., are usefully specifiable as type systems. These are sound and, in the case of distributive analysis frameworks, complete wrt. appropriate natural semantics on abstract properties. Applications include certification of analyses and "optimization" of functional correctness proofs alongside programs. On the example of live variables analysis, we show that analysis type systems are applied versions of more foundational Hoare logics describing either the same abstract property semantics as the type system (liveness states) or a more concrete natural semantics on transition traces of a suitable kind (future defs and uses). The rules of the type system are derivable in the Hoare logic for the abstract property semantics and those in turn in the Hoare logic for the transition trace semantics. This reduction of the burden of trusting the certification vehicle can be compared to foundational proof-carrying code, where general-purpose program logics are preferred to special-purpose type systems and universal logic to program logics. We also look at conditional liveness analysis to see that the same foundational development is also possible for conditional data-flow analyses proceeding from type systems for combined "standard state and abstract property" semantics.

Abstract
The multiary version of the lambda-calculus with generalized applications integrates smoothly both a fragment of sequent calculus and the system of natural deduction of von Plato. It is equipped with reduction rules (corresponding to cut-elimination/normalisation rules) and permutation rules, typical of sequent calculus and of natural deduction with generalised elimination rules. We argue that this system is a suitable tool for doing structural proof theory as rewriting. As an illustration, we investigate combinations of reduction and permutation rules and whether these combinations induce rewriting systems which are confluent and terminating. In some cases, the combination allows the simulation of non-terminating reduction sequences known from explicit substitution calculi. In other cases, we succeed in capturing interesting classes of derivations as the normal forms w.r.t. well-behaved combinations of rules. We identify six of these "combined" normal forms, among which are two classes, due to Herbelin and Mints, in bijection with normal, ordinary natural deductions. A computational explanation for the variety of "combined" normal forms is the existence of three ways of expressing multiple application in the calculus.