Catálogo de publicaciones - libros

There is growing public concern about personal data collected by both private and public sectors. People have very little control over what kinds of data are stored and how such data is used. Moreover, the ability to infer new knowledge from existing data is increasing rapidly with advances in database and data mining technologies. We describe a solution which allows people to take control by specifying constraints on the ways in which their data can be used. User constraints are represented in formal logic, and organizations that want to use this data provide formal proofs that the software they use to process data meets these constraints. Checking the proof by an independent verifier demonstrates that user constraints are (or are not) respected by this software. Our notion of “privacy correctness” differs from general software correctness in two ways. First, properties of interest are simpler and thus their proofs should be easier to automate. Second, this kind of correctness is stricter; in addition to showing a certain relation between input and output is realized, we must also show that only operations that respect privacy constraints are applied during execution. We have therefore an intensional notion of correctness, rather that the usual extensional one. We discuss how our mechanism can be put into practice, and we present the technical aspects via an example. Our example shows how users can exercise control when their data is to be used as input to a decision tree learning algorithm. We have formalized the example and the proof of preservation of privacy constraints in Coq.

We explore foundational typing support for strong updates — updating a memory cell to hold values of unrelated types at different points in time. We present a simple, but expressive type system based upon standard linear logic, one that also enjoys a simple semantic interpretation for types that is closely related to models for spatial logics. The typing interpretation is strong enough that, in spite of the fact that our core calculus supports shared, mutable references and cyclic graphs, every well-typed program terminates. We then consider extensions needed to make our calculus expressive enough to serve as a model for languages with ML-style references, where the capability to access a reference cell is unrestricted, but strong updates are disallowed. Our extensions include a thaw primitive for temporarily re-gaining the capability to perform strong updates on unrestricted references.

Fiore, Plotkin and Turi provided a definition of binding signature and characterised the presheaf of terms generated from a binding signature by an initiality property. Tanaka did for linear binders what Fiore et al did for cartesian binders. They used presheaf categories to model variable binders for contexts, with leading examples given by the untyped ordinary and linear λ -calculi. Here, we give an axiomatic framework that includes their works on cartesian and linear binders, and moreover their assorted variants, notably including the combined cartesian and linear binders of the Logic of Bunched Implications. We provide a definition of binding signature in general, extending the previous ones and yielding a definition for the first time for the example of Bunched Implications, and we characterise the presheaf of terms generated from the binding signature. The characterisation requires a subtle analysis of a strength of a binding signature over a substitution monoidal structure on the presheaf category.

The Focal language (formerly FoC) allows one to incrementally build modules and to formally prove their correctness. In this paper, we present two formal semantics for encoding Focal constructions in the Coq proof assistant. The first one is implemented in the Focal compiler to have the correctness of Focal libraries verified with the Coq proof-checker. The second one formalizes the Focal structures and their main properties as Coq terms (called mixDrecs). The relations between the two embeddings are examined in the last part of the paper.

Higher-order encodings use functions provided by one language to represent variable binders of another. They lead to concise and elegant representations, which historically have been difficult to analyze and manipulate. In this paper we present the $\nabla$ -calculus, a calculus for defining general recursive functions over higher-order encodings. To avoid problems commonly associated with using the same function space for representations and computations, we separate one from the other. The simply-typed λ -calculus plays the role of the representation-level. The computation-level contains not only the usual computational primitives but also an embedding of the representation-level. It distinguishes itself from similar systems by allowing recursion under representation-level λ -binders while permitting a natural style of programming which we believe scales to other logical frameworks. Sample programs include bracket abstraction, parallel reduction, and an evaluator for a simple language with first-class continuations.

The objective of this paper is to develop a functional programming language for quantum computers. We develop a lambda calculus for the classical control model, following the first author’s work on quantum flow-charts. We define a call-by-value operational semantics, and we give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.

This paper studies continuity of the normal form and the context operators as functions in the infinitary lambda calculus. We consider the Scott topology on the cpo of the finite and infinite terms with the prefix relation. We prove that the only continuous parametric trees are Böhm and Lévy–Longo trees. We also prove a general statement: if the normal form function is continuous then so is the model induced by the normal form; as well as the converse for parametric trees. This allows us to deduce that the only continuous models induced by the parametric trees are the ones of Böhm and Lévy–Longo trees. As a first application, we prove that there is an injective embedding from the infinitary lambda calculus of the ∞ η -Böhm trees in D _ ∞ . As a second application, we study the relation between the Scott topology on the prefix relation and the tree topologies. This allows us to prove that the only parametric tree topologies in which all context operators are continuous and the approximation property holds are the ones of Böhm and Lévy–Longo. As a third application, we give an explicit characterisation of the open sets of the Böhm and Lévy–Longo tree topologies.

Two common misbeliefs about encodings of the λ -calculus in interaction nets (INs) are that they are good only for strategies that are not very well understood ( e.g. optimal reduction) and that they always have to deal in a complex way with boxes . In brief, the theory of interaction nets is more or less disconnected from the standard theory: we can do things in INs that we cannot do with terms, which is true [5,10]; and we cannot do in INs things that can easily be done with terms. This paper contributes to fighting this misbelief by showing that the standard call-by-name and call-by-value strategies of the λ -calculus are encoded in interaction nets in a very simple and extensible way, and in particular that these encodings do not need any notion of box. This work can also be seen as a first step towards a generic approach to derive graph-based abstract machines.

α Prolog is a logic programming language which is well-suited for rapid prototyping of type systems and operational semantics of typed λ -calculi and many other languages involving bound names. In α Prolog, the nominal unification algorithm of Urban, Pitts and Gabbay is used instead of first-order unification. However, although α Prolog can be viewed as Horn-clause logic programming in Pitts’ nominal logic , proof search using nominal unification is incomplete in nominal logic. Because of nominal logic’s equivariance principle , complete proof search would require solving NP-hard equivariant unification problems. Nevertheless, the α Prolog programs we studied run correctly without equivariant unification. In this paper, we give several examples of α Prolog programs that do not require equivariant unification, develop a test for identifying such programs, and prove the correctness of this test via a proof-theoretic argument.

This work proposes a type system for checking Abstract Non-Interference in the setting of simply-typed lambda calculus with basic types and recursion. A lambda-expression satisfies Abstract Non-Interference relatively to a given semantic property if an attacker which can only see program data up to that property cannot infer, by observing a computation, private data from public ones. Attackers are abstract interpretations of program semantics. The type analysis infers, for an expression, a security type which approximates the secret kernel for the expression, i.e. the most powerful harmless attacker for which the expression is secure. The type system is proven to be correct, that is, private information is not revealed to an attacker which is unable to distinguish different values belonging to the inferred type.