Trends in Functional Programming Volume 7
eBook - ePub

Trends in Functional Programming Volume 7

  1. 244 pages
  2. English
  3. ePUB (mobile friendly)
  4. Available on iOS & Android
eBook - ePub

Trends in Functional Programming Volume 7

About this book

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.

Frequently asked questions

Yes, you can cancel anytime from the Subscription tab in your account settings on the Perlego website. Your subscription will stay active until the end of your current billing period. Learn how to cancel your subscription.
No, books cannot be downloaded as external files, such as PDFs, for use outside of Perlego. However, you can download books within the Perlego app for offline reading on mobile or tablet. Learn more here.
Perlego offers two plans: Essential and Complete
  • Essential is ideal for learners and professionals who enjoy exploring a wide range of subjects. Access the Essential Library with 800,000+ trusted titles and best-sellers across business, personal growth, and the humanities. Includes unlimited reading time and Standard Read Aloud voice.
  • Complete: Perfect for advanced learners and researchers needing full, unrestricted access. Unlock 1.4M+ books across hundreds of subjects, including academic and specialized titles. The Complete Plan also includes advanced features like Premium Read Aloud and Research Assistant.
Both plans are available with monthly, semester, or annual billing cycles.
We are an online textbook subscription service, where you can get access to an entire online library for less than the price of a single book per month. With over 1 million books across 1000+ topics, we’ve got you covered! Learn more here.
Look out for the read-aloud symbol on your next book to see if you can listen to it. The read-aloud tool reads text aloud for you, highlighting the text as it is being read. You can pause it, speed it up and slow it down. Learn more here.
Yes! You can use the Perlego app on both iOS or Android devices to read anytime, anywhere — even offline. Perfect for commutes or when you’re on the go.
Please note we cannot support devices running on iOS 13 and Android 7 or earlier. Learn more about using the app.
Yes, you can access Trends in Functional Programming Volume 7 by Henrik Nilsson in PDF and/or ePUB format, as well as other popular books in Computer Science & Computer Science General. We have over one million books available in our catalogue for you to explore.

Information

Publisher
Intellect Books
Year
2005
Print ISBN
9781841501888
eBook ISBN
9781841509938
Edition
1
Topic
Computer Science
Subtopic
Computer Science General
Index
Computer Science

Chapter 1

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

Jean-François Monin1, Judicaël Courant1
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 [14].

1.1 INTRODUCTION

This work originates in the verification of a cryptographic system in the Coq proof assistant [14]. In the course of this verification, we modelized plaintext and encrypted data as first-order sorted terms2. For instance, a typical term could be {K1 ⊕ 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 ⊕ 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 [20, 6, 8, 10].
Deduction in presence of a non-trivial equational theory in the general case is notoriously difficult: [15] 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 resul...

Table of contents

  1. Cover
  2. Title Page
  3. Copyright
  4. Contents
  5. Preface
  6. 1. Proving Termination Using Dependent Types: the Case of Xor-Terms
  7. 2. Proving the Correctness of Algorithmic Debugging for Functional Programs
  8. 3. Systematic Synthesis of Functions
  9. 4. A Purely Functional Implementation of ROBDDs in Haskell
  10. 5. Efficient Interpretation by Transforming Data Types and Patterns to Functions
  11. 6. Object-Oriented Programming in Dependent Type Theory
  12. 7. A Sharing Analysis for SAFE
  13. 8. Memory Usage Improvement Using Runtime Alias Detection
  14. 9. A Model of Functional Programming with Dynamic Compilation and Optimization
  15. 10. Functional Concepts in C++
  16. 11. Resource-Based Web Applications
  17. 12. Extensible and Modular Generics for the Masses
  18. 13. When is an Abstract Data Type a Functor?