Trends in Functional Programming (Trends in Functional Programming, 7, Band 7) - Softcover

Softcover

ISBN 10: 1841501883 ISBN 13: 9781841501888

Verlag: Intellect Books, 1999

Inhaltsangabe

This is Volume 7 of Trends in Functional Programming (TFP). It contains a refereed selection of the papers that were presented at TFP 2006: the Seventh Symposium on Trends in Functional Programming. which took place in Nottingham, 19-21 April, 2006.TFP is an international forum for researchers from all functional programming communities spanning the entire width of topics in the field. Its goal is to provide a broad view of current and future trends in functional programming in a lively and friendly setting, thus promoting new research directions related to the field of functional programming and the relationship between functional programming and other fields of computer science.True to the spirit of TFP, the selection of papers in this volume covers a wide range of topics, including dependently typed programming, generic programming, purely functional data structures, function synthesis, declarative debugging, implementation of functional programming languages, and memory management. A particular emerging trend is that of dependently typed programming, reflected by a number of papers in the present selection and by the co-location of TFP and Types 2006.

Über diesen Titel

Auszug. © Genehmigter Nachdruck. Alle Rechte vorbehalten.

Trends in Functional Programming Volume 7

By Henrik Nilsson

Intellect Ltd

Copyright © 2007 Intellect
All rights reserved.

ISBN: 978-1-84150-188-8

Contents

Preface, 
1 Proving Termination Using Dependent Types: the Case of Xor-Terms Jean-François Monin, Judicaël Courant, 
2 Proving the Correctness of Algorithmic Debugging for Functional Programs Yong Luo, Olaf Chitil, 
3 Systematic Synthesis of Functions Pieter Koopman, Rinus Plasmeijer, 
4 A Purely Functional Implementation of ROBDDs in Haskell Jan Christiansen, Frank Huch, 
5 Efficient Interpretation by Transforming Data Types and Patterns to Functions Jan Martin Jansen, Pieter Koopman, Rinus Plasmeijer, 
6 Object-Oriented Programming in Dependent Type Theory Anton Setzer, 
7 A Sharing Analysis for SAFE Ricardo Peña, Clara Segura, Manuel Montenegro, 
8 Memory Usage Improvement Using Runtime Alias Detection Ryo Hanai, Tomoharu Ugawa, Masashi Yoneda, Masahiro Yasugi, Taiichi Yuasa, 
9 A Model of Functional Programming with Dynamic Compilation and Optimization Martin Grabmüller, 
10 Functional Concepts in C++ Rose H. Abdul Rauf, Ulrich Berger, Anton Setzer, 
11 Resource-Based Web Applications Sebastian Fischer, 
12 Extensible and Modular Generics for the Masses Bruno C. d. S. Oliveira, Ralf Hinze, Andres Löh, 
13 When is an Abstract Data Type a Functor? Pablo Nogueira, 

CHAPTER 1

Proving Termination Using Dependent Types: the Case of Xor-Terms

Jean-François Monin, Judicaël Courant

Abstract: We study a normalization function in an algebra of terms quotiented by an associative, commutative and involutive operator (logical xor). This study is motivated by the formal verification of cryptographic systems, relying on a normalization function for xor-terms. Such a function is easy to define using general recursion. However, as it is to be used in a type theoretic proof assistant, we also need a proof of its termination. Instead of using a mixture of various rewriting orderings, we follow an approach involving the power of Type Theory with dependent types. The results are to be applied in the proof of the security API described in.

1.1 INTRODUCTION

This work originates in the verification of a cryptographic system in the Coq proof assistant. In the course of this verification, we modelized plaintext and encrypted data as first-order sorted terms. For instance, a typical term could be {K1 [direct sum] K2}H(KM,H(EXP,KP)) where {x}y denotes encryption of x using a key y, H(x,y) denotes the fingerprint (cryptographic checksum) of the pair (x, y), x [direct sum] y denotes the bitwise exclusive or of x and y. The cryptographic primitives {_}_ and H are commonly supposed to be perfect, and can thus be treated as free constructors. On the contrary, we need to deal with the equational theory of the exclusive or function as many (potential or effective) attacks are based on its algebraic properties.

Deduction in presence of a non-trivial equational theory in the general case is notoriously difficult: shows that the matching problem in the presence of an associative-commutative (AC) function symbol is NP-complete, even in very restricted cases, and AC matching is still an active research topic. In order to solve our particular problem, we only needed a way to define a canonical form for closed terms and a proof of existence of a canonical form for each term. More precisely, we needed a canonicalization function putting any term into its canonical form. On paper, we would use results from term rewriting theory in order to prove the existence of a normalization function with respect to some rewriting system. Unfortunately, the formalization of these results in Coq is only partial yet. Therefore we tried to apply the methods of terms rewriting theory to our problem but stopped when we realized the amount of work needed to complete the definition of the normalization function (section 1.2).

Then we observed that the existence of such a normalization function could be reduced to the existence of a normalization function for terms built over [direct sum] and 0 only. In other words, we can layer our terms into alternating levels of free and non-free constructors, and normalization of the overall term can be deduced from the normalization of all layers (section 1.3).

We formalized such a proof in Coq (section 1.4). Our results are to be applied in our proof of security of an API. However, the approach investigated here is not tied to the specific term algebra of this case study. We reflected this at several places in our formal development, by stating some key definitions and lemmas in an abstract setting, independently of any specific application.

1.2 BACKGROUND

1.2.1 The Need for a Canonicalization Function

In order to reason of our cryptographic system, we need to define some functions or properties over terms. In order to be consistent, we must ensure that these definitions are compatible with the equational theory E induced by commutativity, associativity and cancelation laws of [direct sum] and 0. We can define such a property P using one of the following ways:

• We define P on the whole set of terms (for instance by structural induction). We check afterwards that P is indeed compatible with equality, that is, we check that [MATHEMATICAL EXPRESSION OMITTED]

• We give a canonicalization function N for terms, i.e. a function N from terms to terms such that [MATHEMATICAL EXPRESSION OMITTED]. Then we define P over canonical forms only and extend it in the only compatible way. More formally, we first define some auxiliary predicate P' over terms (for instance by structural induction) and P(t) is defined as P'(N(t)). Thus P is compatible with E by construction.

In our case, the latter approach looks the only reasonable one. For instance, we needed to check whether some secret constant appears in a given term. Let us consider an example: it is clear that KM does not appear in {K1}H(EXP,KEK). But checking that it does not appear in KM [direct sum] {K1} H(EXP,KEK) [direct sum] KM is a bit more difficult, as you have to notice that, although KM syntactically is a subterm of this latter term, the occurences of KM have no semantic significance here because of the self-cancelation law. We therefore do not see how to give a definition for this notion by structural induction on the whole set of terms. On the other hand, once we applied all possible simplication rules (self-cancelation and neutral element cancelation, modulo associativity and commutativity), we just need to check a syntactical occurence of KM.

Therefore, we need to define a canonicalization function N over terms which is also a simplification function, i.e. it ensures that for all term t, no simplification rule applies to N(t).

1.2.2 What Term Rewriting Theory Says

The equational theory of [direct sum] and 0 can be described by the following equations:

[MATHEMATICAL EXPRESSION OMITTED] (1.1)

[MATHEMATICAL EXPRESSION OMITTED] (1.2)

Neutral element x [direct sum] 0 [??] x (1.3)

Involutivity x [direct sum] x [??] 0 (1.4)

Term rewriting theory modulo associativity and commutativity (AC), as described in would say that this equational theory is generated by the following rewrite system,...

Details zur Ausgabe

• Verlag: Intellect Books
• Erscheinungsdatum: 1999
• Sprache: Englisch
• ISBN 10: 1841501883
• ISBN 13: 9781841501888
• Einband: Taschenbuch
• Anzahl der Seiten: 200
• Herausgeber: Nilsson Henrik
• Kontakt zum Hersteller: Nicht verfügbar
• Verantwortliche Person: Nicht verfügbar