| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996465502503316 |
|
|
Titolo |
Theorem Proving in Higher Order Logics [[electronic resource] ] : 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings / / edited by Elsa L. Gunter, Amy Felty |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 1997.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (X, 346 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Computer Science, , 0302-9743 ; ; 1275 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Architecture, Computer |
Computers |
Mathematical logic |
Logic design |
Software engineering |
Computer logic |
Computer System Implementation |
Theory of Computation |
Mathematical Logic and Formal Languages |
Logic Design |
Software Engineering |
Logics and Meanings of Programs |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di contenuto |
|
An Isabelle-based theorem prover for VDM-SL -- Executing formal specifications by translation to higher order logic programming -- Human-style theorem proving using PVS -- A hybrid approach to verifying liveness in a symmetric multi-processor -- Formal verification of concurrent programs in Lp and in Coq: A comparative analysis -- ML programming in constructive type theory -- Possibly infinite sequences in theorem provers: A comparative study -- Proof normalization for a first-order formulation of higher-order logic -- Using a PVS embedding of CSP to verify authentication protocols -- Verifying the accuracy of |
|
|
|
|
|
|
|
|
|
|
|
polynomial approximations in HOL -- A full formalisation of ?-calculus theory in the calculus of constructions -- Rewriting, decision procedures and lemma speculation for automated hardware verification -- Refining reactive systems in HOL using action systems -- On formalization of bicategory theory -- Towards an object-oriented progification language -- Verification for robust specification -- A theory of structured model-based specifications in Isabelle/HOL -- Proof presentation for Isabelle -- Derivation and use of induction schemes in higher-order logic -- Higher order quotients and their implementation in Isabelle HOL -- Type classes and overloading in higher-order logic -- A comparative study of Coq and HOL. |
|
|
|
|
|
|
Sommario/riassunto |
|
This book constitutes the refereed proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '97, held in Murray Hill, NJ, USA, in August 1997. The volume presents 19 carefully revised full papers selected from 32 submissions during a thorough reviewing process. The papers cover work related to all aspects of theorem proving in higher order logics, particularly based on secure mechanization of those logics; the theorem proving systems addressed include Coq, HOL, Isabelle, LEGO, and PVS. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNISA996465948703316 |
|
|
Titolo |
Computer Analysis of Images and Patterns [[electronic resource] ] : 10th International Conference, CAIP 2003, Groningen, The Netherlands, August 25-27, 2003, Proceedings / / edited by Nicolai Petkov, Michel A. Westenberg |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2003.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XVIII, 786 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Computer Science, , 0302-9743 ; ; 2756 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Optical data processing |
Natural language processing (Computer science) |
Computer graphics |
Pattern recognition |
Image Processing and Computer Vision |
Science, Humanities and Social Sciences, multidisciplinary |
Natural Language Processing (NLP) |
Computer Graphics |
Pattern Recognition |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
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 |
|
Analysis and Understanding -- Video -- Segmentation -- Shape -- Classification -- Face Recognition -- Interpolation and Spatial Transformations -- Filtering. |
|
|
|
|
|
|
|
|
Sommario/riassunto |
|
This volume presents the proceedings of the 10th International Conference on Computer Analysis of Images and Patterns (CAIP 2003). This conference - ries started about 18 years ago in Berlin. Initially, the conference served as a forum for meetings between scientists from Western- and Eastern-bloc co- tries. Nowadays, the conference attracts participants from all over the world. The conference gives equal weight to posters and oral presentations, and the selected presentation mode is based on the most appropriate communication medium. The programme follows a single-track format, rather than parallel s- sions. |
|
|
|
|
|
|
|
|
|
|
Non-overlapping oral and poster sessions ensure that all attendees have the opportunity to interact personally with presenters. As for the numbers, we received a total of 160 submissions. All papers were reviewed by two to three members of the Programme Committee. The ?nal - lection was carried out by the Conference Chairs. Out of the 160 papers, 42 were selected for oral presentation and 52 as posters. At this point, we wish to thank the Programme Committee and additional referees for their timely and high-quality reviews. The paper submission and review procedure was carried out electronically. We thank Marcin Morg´ os from Scalar–IT Solutions for p- viding us with the Web-based participant registration system. We also thank the invited speakers Nicholas Ayache, John Daugman, and Dariu Gavrila, for kindly accepting our invitation. |
|
|
|
|
|
| |