My Account Log in

1 option

Types for Proofs and Programs : International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers / edited by Jean-Christophe Filliatre, Christine Paulin-Mohring, Benjamin Werner.

SpringerLink Books Lecture Notes In Computer Science (LNCS) (1997-2024) Available online

View online
Format:
Book
Contributor:
Filliâtre, Jean-Christophe, editor.
Paulin-Mohring, Christine, 1962- editor.
Werner, Benjamin, editor.
SpringerLink (Online service)
Series:
Computer Science (Springer-11645)
LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 3839.
Theoretical Computer Science and General Issues ; 3839
Language:
English
Subjects (All):
Computer logic.
Programming languages (Electronic computers).
Logic, Symbolic and mathematical.
Computer science--Mathematics.
Computer science.
Artificial intelligence.
Logics and Meanings of Programs.
Programming Languages, Compilers, Interpreters.
Mathematical Logic and Formal Languages.
Symbolic and Algebraic Manipulation.
Artificial Intelligence.
Local Subjects:
Logics and Meanings of Programs.
Programming Languages, Compilers, Interpreters.
Mathematical Logic and Formal Languages.
Symbolic and Algebraic Manipulation.
Artificial Intelligence.
Physical Description:
1 online resource (VIII, 280 pages).
Edition:
First edition 2006.
Contained In:
Springer eBooks
Place of Publication:
Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2006.
System Details:
text file PDF
Contents:
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.
Other Format:
Printed edition:
ISBN:
978-3-540-31429-5
9783540314295
Access Restriction:
Restricted for use by site license.

The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.

Find

Home Release notes

My Account

Shelf Request an item Bookmarks Fines and fees Settings

Guides

Using the Find catalog Using Articles+ Using your account