Theorem Proving in Higher Order Logics 13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14-18, 2000 Proceedings /
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...
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg : Imprint: Springer,
2000.
|
| Έκδοση: | 1st ed. 2000. |
| Σειρά: | Lecture Notes in Computer Science,
1869 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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.
