Research in Computational Molecular Biology [[electronic resource] ] : 10th Annual International Conference, RECOMB 2006, Venice, Italy, April 2-5, 2006, Proceedings / / edited by Alberto Apostolico, Concettina Guerra, Sorin Istrail, Pavel Pevzner, Michael Waterman

• Record Nr.: UNISA996466108603316
• Pubbl/distr/stampa: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006
• ISBN: 3-540-33296-0
• Edizione: [1st ed. 2006.]
• Descrizione fisica: 1 online resource (XVIII, 614 p.)
• Collana: Lecture Notes in Bioinformatics ; ; 3909
• Disciplina: 572.8
• Soggetti: Algorithms; Data structures (Computer science); Computer science—Mathematics; Database management; Artificial intelligence; Bioinformatics; Algorithm Analysis and Problem Complexity; Data Structures; Discrete Mathematics in Computer Science; Database Management; Artificial Intelligence
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Integrated Protein Interaction Networks for 11 Microbes -- Hypergraph Model of Multi-residue Interactions in Proteins: Sequentially–Constrained Partitioning Algorithms for Optimization of Site-Directed Protein Recombination -- Biological Networks: Comparison, Conservation, and Evolutionary Trees -- Assessing Significance of Connectivity and Conservation in Protein Interaction Networks -- Clustering Short Gene Expression Profiles -- A Patient-Gene Model for Temporal Expression Profiles in Clinical Studies -- Global Interaction Networks Probed by Mass Spectrometry -- Statistical Evaluation of Genome Rearrangement -- An Improved Statistic for Detecting Over-; Represented Gene Ontology Annotations in Gene Sets -- Protein Function Annotation Based on Ortholog Clusters Extracted from Incomplete Genomes Using Combinatorial Optimization -- Detecting MicroRNA Targets by Linking Sequence, MicroRNA and Gene Expression Data -- RNA Secondary Structure Prediction Via Energy Density Minimization -- Structural Alignment of Pseudoknotted RNA -- Stan Ulam and Computational Biology -- CONTRAlign: Discriminative Training for Protein Sequence Alignment -- Clustering Near-Identical Sequences for Fast Homology Search -- New Methods for Detecting Lineage-Specific Selection -- A Probabilistic Model for Gene Content Evolution with Duplication, Loss, and Horizontal Transfer -- A Sublinear-Time Randomized Approximation Scheme for the Robinson-Foulds Metric -- Algorithms to Distinguish the Role of Gene-Conversion from Single-Crossover Recombination in the Derivation of SNP Sequences in Populations -- Inferring Common Origins from mtDNA -- Efficient Enumeration of Phylogenetically Informative Substrings -- Phylogenetic Profiling of Insertions and Deletions in Vertebrate Genomes -- Maximal Accurate Forests from Distance Matrices -- Leveraging Information Across HLA Alleles/Supertypes Improves Epitope Prediction -- Improving Prediction of Zinc Binding Sites by Modeling the Linkage Between Residues Close in Sequence -- An Important Connection Between Network Motifs and Parsimony Models -- Ultraconserved Elements, Living Fossil Transposons, and Rapid Bursts of Change: Reconstructing the Uneven Evolutionary History of the Human Genome -- Permutation Filtering: A Novel Concept for Significance Analysis of Large-Scale Genomic Data -- Genome-Wide Discovery of Modulators of Transcriptional Interactions in Human B Lymphocytes -- A New Approach to Protein Identification -- Markov Methods for Hierarchical Coarse-Graining of Large Protein Dynamics -- Simulating Protein Motions with Rigidity Analysis -- Predicting Experimental Quantities in Protein Folding Kinetics Using Stochastic Roadmap Simulation -- An Outsider’s View of the Genome -- Alignment Statistics for Long-Range Correlated Genomic Sequences -- Simple and Fast Inverse Alignment -- Revealing the Proteome Complexity by Mass Spectrometry -- Motif Yggdrasil: Sampling from a Tree Mixture Model -- A Study of Accessible Motifs and RNA Folding Complexity -- A Parameterized Algorithm for Protein Structure Alignment -- Geometric Sieving: Automated Distributed Optimization of 3D Motifs for Protein Function Prediction -- A Branch-and-Reduce Algorithm for the Contact Map Overlap Problem -- A Novel Minimized Dead-End Elimination Criterion and Its Application to Protein Redesign in a Hybrid Scoring and Search Algorithm for Computing Partition Functions over Molecular Ensembles -- 10 Years of the International Conference on Research in Computational Molecular Biology (RECOMB) -- Sorting by Weighted Reversals, Transpositions, and Inverted Transpositions -- A Parsimony Approach to Genome-Wide Ortholog Assignment -- Detecting the Dependent Evolution of Biosequences -- Detecting MicroRNA Targets by Linking Sequence, MicroRNA and Gene Expression Data.

Theorem Proving in Higher Order Logics : 13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14-18, 2000 Proceedings / / edited by Mark Aagaard, John Harrison

• Record Nr.: UNINA9910767567003321
• Pubbl/distr/stampa: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000
• ISBN: 1-280-95654-2; 9786610956548; 3-540-44659-1
• Edizione: [1st ed. 2000.]
• Descrizione fisica: 1 online resource (545 p.)
• Collana: Lecture Notes in Computer Science, , 1611-3349 ; ; 1869
• Disciplina: 004.015113
• Soggetti: Artificial intelligence; Computer science; Compilers (Computer programs); Machine theory; Software engineering; Artificial Intelligence; Theory of Computation; Compilers and Interpreters; Formal Languages and Automata Theory; Computer Science Logic and Foundations of Programming; Software Engineering
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: Description based upon print version of record.
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Fix-Point Equations for Well-Founded Recursion in Type Theory -- Programming and Computing in HOL -- Proof Terms for Simply Typed Higher Order Logic -- Routing Information Protocol in HOL/SPIN -- Recursive Families of Inductive Types -- Aircraft Trajectory Modeling and Alerting Algorithm Verification -- Intel’s Formal Verification Experience on the Willamette Development -- A Prototype Proof Translator from HOL to Coq -- Proving ML Type Soundness Within Coq -- On the Mechanization of Real Analysis in Isabelle/HOL -- Equational ; Reasoning via Partial Reflection -- Reachability Programming in HOL98 Using BDDs -- Transcendental Functions and Continuity Checking in PVS -- Verified Optimizations for the Intel IA-64 Architecture -- Formal Verification of IA-64 Division Algorithms -- Fast Tactic-Based Theorem Proving -- Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover -- A Strong and Mechanizable Grand Logic -- Inheritance in Higher Order Logic: Modeling and Reasoning -- Total-Correctness Refinement for Sequential Reactive Systems -- Divider Circuit Verification with Model Checking and Theorem Proving -- Specification and Verification of a Steam-Boiler with Signal-Coq -- Functional Procedures in Higher-Order Logic -- Formalizing Stålmarck’s Algorithm in Coq -- TAS — A Generic Window Inference System -- Weak Alternating Automata in Isabelle/HOL -- Graphical Theories of Interactive Systems: Can a Proof Assistant Help? -- Formal Verification of the Alpha 21364 Network Protocol -- Dependently Typed Records for Representing Mathematical Structure -- Towards a Machine-Checked Java Specification Book -- Another Look at Nested Recursion -- Automating the Search for Answers to Open Questions -- Appendix: Conjectures Concerning Proof, Design, and Verification.
• Sommario/riassunto: This volume is the proceedings of the 13th International Conference on Theo­ rem Proving in Higher Order Logics (TPHOLs 2000) held 14-18 August 2000 in Portland, Oregon, USA. Each of the 55 papers submitted in the full rese­ arch category was refereed by at least three reviewers who were selected by the program committee. Because of the limited space available in the program and proceedings, only 29 papers were accepted for presentation and publication in this volume. In keeping with tradition, TPHOLs 2000 also offered a venue for the presen­ tation of work in progress, where researchers invite discussion by means of a brief preliminary talk and then discuss their work at a poster session. A supplemen­ tary proceedings containing associated papers for work in progress was published by the Oregon Graduate Institute (OGI) as technical report CSE-00-009. The organizers are grateful to Bob Colwell, Robin Milner and Larry Wos for agreeing to give invited talks. Bob Colwell was the lead architect on the Intel P6 microarchitecture, which introduced a number of innovative techniques and achieved enormous commercial success. As such, he is ideally placed to offer an industrial perspective on the challenges for formal verification. Robin Milner contributed many key ideas to computer theorem proving, and to functional programming, through his leadership of the influential Edinburgh LCF project.