Type(s) de contenu et mode(s) de consultation : Texte noté : électronique

Auteur(s) : International workshop TYPES (2004 ; Jouy-en-Josas, Yvelines)  Voir les notices liées en tant qu'auteur

Titre(s) : Types for Proofs and Programs [Texte électronique] : International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers / edited by Jean-Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner

Titre d'ensemble : Types for proofs and programs

Publication : Berlin, Heidelberg : Springer-Verlag Berlin Heidelberg, 2006

Description matérielle : 1 online resource (Online-Datei.)

Collection : Lecture Notes in Computer Science ; 3839

Note(s) : Computer Science (Springer-11645)

Autre(s) auteur(s) : Filliâtre, Jean-Christophe. Éditeur scientifique  Voir les notices liées en tant qu'auteur
Paulin-Mohring, Christine (1962-....). Fonction indéterminée  Voir les notices liées en tant qu'auteur
Werner, Benjamin. Fonction indéterminée  Voir les notices liées en tant qu'auteur

Sujet(s) : Théorèmes -- Démonstration automatique  Voir les notices liées en tant que sujet
Programmation (informatique)  Voir les notices liées en tant que sujet

Genre ou forme : Actes de congrès  Voir les notices liées en tant que genre ou forme

Indice(s) Dewey :  005.131 (23e éd.) = Logique symbolique (informatique)  Voir les notices liées en tant que sujet ; 005.1 (23e éd.) = Développement de logiciels  Voir les notices liées en tant que sujet ; 005.101 5113 (23e éd.) = Développement de logiciels - Logique mathématique  Voir les notices liées en tant que sujet

Identifiants, prix et caractéristiques : ISBN 9783540314295

Voir aussi : Publication alternative dans un autre support/format : Types for proofs and programs [Texte imprimé], ISBN 3540314288

Identifiant de la notice  : ark:/12148/cb44685535z

Notice n° :  FRBNF44685535 (notice reprise d'un réservoir extérieur)

Table des matières : 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{u2019}s Set Theory as a PTS with 4 Sorts ; Exploring the Regular Tree Types ; On Constructive Existence.