Skip to main content
  • Conference proceedings
  • © 2006

Types for Proofs and Programs

International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 3839)

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Conference series link(s): TYPES: International Workshop on Types for Proofs and Programs

Conference proceedings info: TYPES 2004.

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (17 papers)

  1. Front Matter

  2. A Content Based Mathematical Search Engine: Whelp

    • Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
    Pages 17-32
  3. A Machine-Checked Formalization of the Random Oracle Model

    • Gilles Barthe, Sabrina Tarento
    Pages 33-49
  4. A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis

    • Yves Bertot, Benjamin Grégoire, Xavier Leroy
    Pages 66-81
  5. Formalising Bitonic Sort in Type Theory

    • Ana Bove, Thierry Coquand
    Pages 82-97
  6. A Semi-reflexive Tactic for (Sub-)Equational Reasoning

    • Claudio Sacerdoti Coen
    Pages 98-114
  7. A Uniform and Certified Approach for Two Static Analyses

    • Solange Coupet-Grimal, William Delobel
    Pages 115-137
  8. A Tool for Automated Theorem Proving in Agda

    • Fredrik Lindblad, Marcin Benke
    Pages 154-169
  9. Surreal Numbers in Coq

    • Lionel Elie Mamane
    Pages 170-185
  10. A Few Constructions on Constructors

    • Conor McBride, Healfdene Goguen, James McKinna
    Pages 186-200
  11. Tactic-Based Optimized Compilation of Functional Programs

    • Thomas Meyer, Burkhart Wolff
    Pages 201-214
  12. Interfaces as Games, Programs as Strategies

    • Markus Michelbrink
    Pages 215-231
  13. λZ: Zermelo’s Set Theory as a PTS with 4 Sorts

    • Alexandre Miquel
    Pages 232-251
  14. Exploring the Regular Tree Types

    • Peter Morris, Thorsten Altenkirch, Conor McBride
    Pages 252-267
  15. On Constructive Existence

    • Michel Parigot
    Pages 268-273
  16. Back Matter

Other Volumes

  1. Types for Proofs and Programs

Editors and Affiliations

  • LRI, Univ Paris-Sud, CNRS, Orsay F-91405, INRIA Futurs, ProVal, Orsay

    Jean-Christophe Filliâtre

  • INRIA Saclay - Île-de-France, ProVal - Orsay 91893 and LRI, Univ Paris-Sud, CNRS - Orsay 91405LRI, Université Paris Sud and INRIA Futurs, Bât. 490, Université Paris Sud, Orsay Cedex, France

    Christine Paulin-Mohring

  • INRIA-Futurs at, LIX, École Polytechnique, Palaiseau, France

    Benjamin Werner

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access