このページのリンク

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
(Theoretical Computer Science and General Issues. ISSN:25122029 ; 3839)

データ種別 電子ブック
1st ed. 2006.
出版者 (Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer)
出版年 2006
大きさ VIII, 280 p : online resource
著者標目 Filliatre, Jean-Christophe editor
Paulin-Mohring, Christine editor
Werner, Benjamin editor
SpringerLink (Online service)

所蔵情報を非表示

URL
射水-電子 007 EB0003943 Computer Scinece R0 2005-6,2022-3

9783540314295

書誌詳細を非表示

一般注記 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
HTTP:URL=https://doi.org/10.1007/11617990
件 名 LCSH:Computer science
LCSH:Compilers (Computer programs)
LCSH:Machine theory
LCSH:Computer science -- Mathematics  全ての件名で検索
LCSH:Artificial intelligence
FREE:Computer Science Logic and Foundations of Programming
FREE:Compilers and Interpreters
FREE:Formal Languages and Automata Theory
FREE:Symbolic and Algebraic Manipulation
FREE:Artificial Intelligence
分 類 LCC:QA75.5-76.95
DC23:004.0151
書誌ID EB00003331
ISBN 9783540314295

 類似資料