Skip to main content
SpringerLink
Log in
Book cover

Types for Proofs and Programs

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

  • Conference proceedings
  • © 2006

Overview

Editors:
  1. Jean-Christophe Filliâtre

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

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Christine Paulin-Mohring

    1. 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

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Benjamin Werner

    1. INRIA-Futurs at, LIX, École Polytechnique, Palaiseau, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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)

Included in the following conference series:

Conference proceedings info: TYPES 2004.

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

Access this book

Log in via an institution
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

Licence this eBook for your library

Institutional subscriptions

Table of contents (17 papers)

  1. Front Matter

    Download chapter PDF

  2. Formalized Metatheory with Terms Represented by an Indexed Family of Types

    • Robin Adams
    Pages 1-16

  3. A Content Based Mathematical Search Engine: Whelp

    • Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
    Pages 17-32

  4. A Machine-Checked Formalization of the Random Oracle Model

    • Gilles Barthe, Sabrina Tarento
    Pages 33-49

  5. Extracting a Normalization Algorithm in Isabelle/HOL

    • Stefan Berghofer
    Pages 50-65

  6. A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis

    • Yves Bertot, Benjamin Grégoire, Xavier Leroy
    Pages 66-81

  7. Formalising Bitonic Sort in Type Theory

    • Ana Bove, Thierry Coquand
    Pages 82-97

  8. A Semi-reflexive Tactic for (Sub-)Equational Reasoning

    • Claudio Sacerdoti Coen
    Pages 98-114

  9. A Uniform and Certified Approach for Two Static Analyses

    • Solange Coupet-Grimal, William Delobel
    Pages 115-137

  10. Solving Two Problems in General Topology Via Types

    • Adam Grabowski
    Pages 138-153

  11. A Tool for Automated Theorem Proving in Agda

    • Fredrik Lindblad, Marcin Benke
    Pages 154-169

  12. Surreal Numbers in Coq

    • Lionel Elie Mamane
    Pages 170-185

  13. A Few Constructions on Constructors

    • Conor McBride, Healfdene Goguen, James McKinna
    Pages 186-200

  14. Tactic-Based Optimized Compilation of Functional Programs

    • Thomas Meyer, Burkhart Wolff
    Pages 201-214

  15. Interfaces as Games, Programs as Strategies

    • Markus Michelbrink
    Pages 215-231

  16. λZ: Zermelo’s Set Theory as a PTS with 4 Sorts

    • Alexandre Miquel
    Pages 232-251

  17. Exploring the Regular Tree Types

    • Peter Morris, Thorsten Altenkirch, Conor McBride
    Pages 252-267

  18. On Constructive Existence

    • Michel Parigot
    Pages 268-273

  19. Back Matter

    Download chapter PDF
Back to top

Other volumes

  1. Types for Proofs and Programs

Keywords

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

Publish with us

Policies and ethics

Back to top

Search

Navigation