Types for proofs and programs
Authors
Parameters
More about the book
InhaltsverzeichnisFormalized 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.
Book purchase
Types for proofs and programs, Jean-Christophe Filliâtre
- Language
- Released
- 2006
Payment methods
- Title
- Types for proofs and programs
- Language
- English
- Authors
- Jean-Christophe Filliâtre
- Publisher
- Springer
- Released
- 2006
- ISBN10
- 3540314288
- ISBN13
- 9783540314288
- Series
- Lecture notes in computer science
- Category
- Computers, IT, Programming
- Description
- InhaltsverzeichnisFormalized 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.