Types for Proofs and Programs
International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers
Published on 25. January 2006
Book
Paperback/Softback
VIII, 280 pages
978-3-540-31428-8 (ISBN)
Description
The 17 revised full papers presented here cover all current issues of formal reasoning and computer programming based on type theory are addressed; in particular languages and computerised tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalisation of mathematics and mathematics education.
More details
Series
Edition
2006 ed.
Language
English
Place of publication
Berlin
Germany
Publishing group
Springer Berlin
Target group
Professional and scholarly
Research
Illustrations
VIII, 280 p.
Dimensions
Height: 23.5 cm
Width: 15.5 cm
Weight
910 gr
ISBN-13
978-3-540-31428-8 (9783540314288)
DOI
10.1007/11617990
Schweitzer Classification
Content
Formalized Metatheory with Terms Represented by an Indexed Family of Types.- A Content Based Mathematical Search Engine: Whelp.- A Machine-Checked Formalization of the Random Oracle Model.- Extracting a Normalization Algorithm in Isabelle/HOL.- A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis.- Formalising Bitonic Sort in Type Theory.- A Semi-reflexive Tactic for (Sub-)Equational Reasoning.- A Uniform and Certified Approach for Two Static Analyses.- Solving Two Problems in General Topology Via Types.- A Tool for Automated Theorem Proving in Agda.- Surreal Numbers in Coq.- A Few Constructions on Constructors.- Tactic-Based Optimized Compilation of Functional Programs.- Interfaces as Games, Programs as Strategies.- ?Z: Zermelo's Set Theory as a PTS with 4 Sorts.- Exploring the Regular Tree Types.- On Constructive Existence.