Lo studio storico del mondo antico nella cultura italiana dell'Ottocento : [Incontri perugini di storia della storiografia antica e sul mondo antico, 3., Acquasparta, Palazzo Cesi, 30 maggio-1 giugno 1988] / a cura di Leandro Polverini

• Record Nr.: UNISA990000979490203316
• Pubbl/distr/stampa: Napoli : Edizioni scientifiche italiane, [1993]
• ISBN: 88-7104-831-8
• Descrizione fisica: 473 p. ; 25 cm
• Disciplina: 938.0072045
• Soggetti: Civiltà classica - Studi italiani - Sec. 19
• Collocazione: IX.3. 202(VIII C COLL.174/3)
• Lingua di pubblicazione: Italiano
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Note generali: In testa al front.: Università degli studi di Perugia, Dipartimento di scienze storiche dell'antichità

Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering : New Ideas and Emerging Results / / Institute of Electrical and Electronics Engineers

• Record Nr.: UNINA9910418308503321
• Pubbl/distr/stampa: [Place of publication not identified] : , : IEEE, , 2020
• ISBN: 1-72816-527-X
• Descrizione fisica: 1 online resource
• Disciplina: 006.31
• Soggetti: Machine learning
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia

Theorem Proving in Higher Order Logics : 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings / / edited by Victor A. Carreno, Cesar A. Munoz, Sofiene Tahar

• Record Nr.: UNINA9910768181703321
• Pubbl/distr/stampa: Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002
• ISBN: 3-540-45685-6
• Edizione: [1st ed. 2002.]
• Descrizione fisica: 1 online resource (X, 347 p.)
• Collana: Lecture Notes in Computer Science, , 0302-9743 ; ; 2410
• Disciplina: 004/.01/5113
• Soggetti: Computer architecture; Computers; Software engineering; Logic design; Computer System Implementation; Theory of Computation; Software Engineering; Logic Design
• 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: Invited Talks -- Formal Methods at NASA Langley -- Higher Order Unification 30 Years Later -- Regular Papers -- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction -- Efficient Reasoning about Executable Specifications in Coq -- Verified Bytecode Model Checkers -- The 5 Colour Theorem in Isabelle/Isar -- Type-Theoretic Functional Semantics -- A Proposal for a Formal OCL Semantics in Isabelle/HOL -- Explicit Universes for the Calculus of Constructions -- Formalised Cut Admissibility for Display Logic -- Formalizing the Trading Theorem for the Classification of Surfaces -- Free-Style Theorem Proving -- A Comparison of Two Proof Critics: Power vs. Robustness -- Two-Level Meta-reasoning in Coq -- PuzzleTool: An Example of Programming Computation and Deduction -- A Formal Approach to Probabilistic Termination -- Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm -- Quotient Types: A Modular Approach -- Sequent Schema for Derived Rules -- Algebraic Structures and Dependent Records -- Proving the Equivalence of Microstep and Macrostep Semantics -- Weakest Precondition for General Recursive Programs Formalized in Coq.
• Sommario/riassunto: This book constitutes the refereed proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002, held in Hampton, VA, USA in August 2002.The 20 revised full papers presented together with 2 invited contributions were carefully reviewed and selected from 34 submissions. All current issues in HOL theorem proving and formal verification of software and hardware systems are addressed. Among the HOL theorem proving systems evaluated are Isabelle/HOL, Isabelle/Isar, and Coq.