Types for Proofs and Programs

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

Jean-Christophe Filliatre, Christine Paulin-Mohring, Benjamin Werner (Herausgeber)

Buch | Softcover

VIII, 280 Seiten

2006
Springer Berlin (Verlag)
978-3-540-31428-8 (ISBN)

Artikel merken

lt;p>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.

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.

Erscheint lt. Verlag	25.1.2006
Reihe/Serie	Lecture Notes in Computer Science
Reihe/Serie	Theoretical Computer Science and General Issues
Zusatzinfo	VIII, 280 p.
Verlagsort	Berlin
Sprache	englisch
Maße	155 x 235 mm
Gewicht	910 g
Themenwelt	Informatik ► Theorie / Studium ► Compilerbau
Themenwelt	Informatik ► Theorie / Studium ► Künstliche Intelligenz / Robotik
Schlagworte	algorithm • Calculus • Coq • formal methods • Formal Reasoning • Formal Verification • Optimization • programming • Programming language • Programming Theory • Proof theory • proving • Rewriting Systems • subtyping • theorem proving
ISBN-10	3-540-31428-8 / 3540314288
ISBN-13	978-3-540-31428-8 / 9783540314288
Zustand	Neuware