Catálogo de publicaciones - libros

It is well-known, due to the work of Girard and Coquand, that adding polymorphic domains to higher order logic, HOL, or its type theoretic variant HOL, renders the logic inconsistent. This is known as Girard’s paradox, see [4]. But there is also another presentation of higher order logic, in its type theoretic variant called PRED, to which polymorphic domains can be added safely, Both HOL and PRED are well-known type systems and in this paper we study why HOL with polymorphic domains is inconsistent and why nd PRED with polymorphic domains remains consistent. We do this by describing a simple model for the latter and we show why this can not be a model of the first.

We reconsider the well-known concept of Haskell-style type classes within the logical framework of Isabelle. So far, axiomatic type classes in Isabelle merely account for the logical aspect as predicates over types, while the operational part is only a convention based on raw overloading. Our more elaborate approach to constructive type classes provides a seamless integration with Isabelle locales, which are able to manage both operations and logical properties uniformly. Thus we combine the convenience of type classes and the flexibility of locales. Furthermore, we construct dictionary terms derived from notions of the type system. This additional internal structure provides satisfactory foundations of type classes, and supports further applications, such as code generation and export of theories and theorems to environments without type classes.

Taking a ‘set’ to be a type together with an equivalence relation and adding an extensional choice axiom to the logical framework (a restricted version of constructive type theory) it is shown that any ‘set’ can be well-ordered. Zermelo’s first proof from 1904 is followed, with a simplification to avoid using comparability of well-orderings. The proof has been formalised in the system AgdaLight.

We expose a formalism that allows the expression of any theory with one or more axiom schemes using a finite number of axioms. These axioms have the property of being easily orientable into rewrite rules. This allows us to give finite first-order axiomatizations of arithmetic and real fields theory, and a presentation of arithmetic in deduction modulo that has a finite number of rewrite rules. Overall, this formalization relies on a weak calculus of explicit substitutions to provide a simple and finite framework.

In this article we present a method for formally proving the correctness of the lazy algorithms for computing homographic and quadratic transformations — of which field operations are special cases— on a representation of real numbers by coinductive streams. The algorithms work on coinductive stream of Möbius maps and form the basis of Edalat–Potts exact real arithmetic. We build upon our earlier work of formalising the homographic and quadratic algorithms in constructive type theory via general corecursion. Based on the notion of equations for general corecursive definitions we prove by coinduction the correctness of the algorithms. We use the machinery of the proof assistant for coinductive types to present the formalisation. The material in this article is fully formalised in the proof assistant.

This paper presents a system of cost derivation for higher-order and polymorphic functional programs based on a notion of sized types and exploiting a type-and-effect system approach. The paper gives an operational semantics of cost for a simple strict functional language in terms of -calculus -reduction steps and introduces type rules describing cost effects. The type system is based on intersection types. The use of discrete polymorphism (intersection types) instead of the usual parametric polymorphism approach improves the analysis and solves, in many cases, the “size aliasing problem” that has been identified as a limitation on previous type-and-effect approaches. Finally we provide a proof of the soundness of our effect system with respect to the cost semantics.

We propose a new language for writing programs with dependent types on top of the proof assistant. This language permits to establish a phase distinction between writing and proving algorithms in the environment. Concretely, this means allowing to write algorithms as easily as in a practical functional programming language whilst giving them as rich a specification as desired and proving that the code meets the specification using the whole proof apparatus. This is achieved by extending conversion to an equivalence which relates types and subsets based on them, a technique originating from the “” feature of PVS and following mathematical convention. The typing judgements can be translated to the (CIC) by means of an interpretation which inserts coercions at the appropriate places. These coercions can contain existential variables representing the propositional parts of the final term, corresponding to proof obligations (or PVS type-checking conditions). A prototype implementation of this process is integrated with the environment.

In previous work we have proposed a distributed security logic for authorizing code. To gain assurance about the correctness of the implementation of our system, we now present a series of security logics of increasing expressive power leading up to our logic. We encode each logic in Coq, develop an algorithm for deciding queries, and prove properties about the algorithm in Coq. By using Coq’s automatic extraction mechanism, we are able to gain a high assurance about the resulting reference monitor implementations. Following this strategy yields reference monitors fully certified at the source code level for Datalog, Binder, Binder with a general extension mechanism, and a logic that combines Binder and the calculus of co-inductive constructions.