Skip to main content
SpringerLink
Log in

Types for Proofs and Programs

International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers

  • Conference proceedings
  • © 2008

Overview

Editors:
  1. Marino Miculan
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Ivan Scagnetto
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Furio Honsell
    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 4941)

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

Included in the following conference series:

Conference proceedings info: TYPES 2007.

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 (13 papers)

  1. Front Matter

    Download chapter PDF

  2. Algorithmic Equality in Heyting Arithmetic Modulo

    • Lisa Allali
    Pages 1-17

  3. CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types

    • Robert Atkey
    Pages 18-32

  4. Dependently Sorted Logic

    • João Filipe Belo
    Pages 33-50

  5. Finiteness in a Minimalist Foundation

    • Francesco Ciraulo, Giovanni Sambin
    Pages 51-68

  6. A Declarative Language for the Coq Proof Assistant

    • Pierre Corbineau
    Pages 69-84

  7. Characterising Strongly Normalising Intuitionistic Sequent Terms

    • J. Espírito Santo, S. Ghilezan, J. Ivetić
    Pages 85-99

  8. Intuitionistic vs. Classical Tautologies, Quantitative Comparison

    • Antoine Genitrini, Jakub Kozik, Marek Zaionc
    Pages 100-109

  9. In the Search of a Naive Type Theory

    • Agnieszka Kozubek, PaweÅ‚ Urzyczyn
    Pages 110-124

  10. Verification of the Redecoration Algorithm for Triangular Matrices

    • Ralph Matthes, Martin Strecker
    Pages 125-141

  11. A Logic for Parametric Polymorphism with Effects

    • Rasmus Ejlers Møgelberg, Alex Simpson
    Pages 142-156

  12. Working with Mathematical Structures in Type Theory

    • Claudio Sacerdoti Coen, Enrico Tassi
    Pages 157-172

  13. On Normalization by Evaluation for Object Calculi

    • J. Schwinghammer
    Pages 173-187

  14. Attributive Types for Proof Erasure

    • Hongwei Xi
    Pages 188-202

  15. Back Matter

    Download chapter PDF
Back to top

Other volumes

  1. Types for Proofs and Programs

Keywords

About this book

This book constitutes the thoroughly refereed post-conference proceedings of TYPES 2007, the concluding conference of the Types project, held in Cividale del Friuli, Italy, in May 2007. The 13 revised full papers presented were carefully reviewed and selected from 22 submissions. The topic of this last annual workshop of the Types Working Group was formal reasoning and computer programming based on type theory. Great importance was attached to languages and computerized tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalization of mathematics and mathematics education.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation