Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Types for Proofs and Programs [[electronic resource] ] : 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
| Types for Proofs and Programs [[electronic resource] ] : 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 |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
| Descrizione fisica | 1 online resource (VIII, 280 p.) |
| Disciplina | 005.131 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Compilers (Computer programs) Machine theory Computer science—Mathematics Artificial intelligence Computer Science Logic and Foundations of Programming Compilers and Interpreters Formal Languages and Automata Theory Symbolic and Algebraic Manipulation Artificial Intelligence |
| ISBN | 3-540-31429-6 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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. |
| Record Nr. | UNISA-996466114703316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
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 (eds.)
| 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 (eds.) |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, 2006 |
| Descrizione fisica | 1 online resource (VIII, 280 p.) |
| Disciplina | 005.131 |
| Altri autori (Persone) |
FilliatreJean-Christophe
Paulin-MohringChristine <1962-> WernerBenjamin |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Automatic theorem proving
Computer programming |
| ISBN | 3-540-31429-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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. |
| Altri titoli varianti | TYPES 2004 |
| Record Nr. | UNINA-9910483584903321 |
| Berlin ; ; New York, : Springer, 2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||