TPHOLs'99: Paper Submission

Category:	Formal research paper	Work in progress paper
Paper Title:
Contact name:
Contact e-mail:
Contact fax:	(Include country and area codes)
Submission Format:	Postscript	PDF
You submission must be in either Postscript or PDF format.
Compression Used:	GNU gzip	UNIX compress	None
To save bandwidth you may compress your submission.
Submission file:

Please use the options below to indicate which, if any, systems your paper discusses.

ACL2	Alf	Coq	Elf
HOL	IMPS	Isabelle/HOL	Isabelle
Lambda-Prolog	Lego	Mizar	Nuprl
NqThm	PVS	other:

Please use the options below to describe the content areas of your paper. If your paper touches on many of these areas then it it will be more helpful if you indicate only those areas that form the focus of the paper.

1. Implementation and Verification of Theorem Provers 1.1 Implementation and verification of theorem provers in general 1.2 Reflection 1.3 Verifying decision procedures 1.4 Verifying theorem provers 1.5 Recording and checking proofs	2. Proof Automation 2.1 Proof automation in general 2.2 Automating proof in higher order logics 2.3 Proof strategies and planning 2.4 Decision procedures 2.5 Rewriting 2.6 Model checking 2.7 Inductive and co-inductive definitions 2.8 Inductive theorem proving
3. Interactive Reasoning 3.1 Interactive reasoning in general 3.2 Tactic based theorem proving 3.3 Design of tactics 3.4 Applications for meta-variables	4. Human Prover Interaction 4.1 User interfaces to theorem provers 4.2 Proof presentation 4.3 Theory presentation
5. Inter-operation 5.1 Linking theorem provers together 5.2 Incorporating provers into larger systems 5.3 Linking provers and external decision procedures 5.4 Linking provers and computer algebra systems	6. Logical Aspects 6.1 Logical aspects in general 6.2 Set theory 6.3 Constructive type theory 6.4 Proof theory 6.5 Temporal logic 6.6 Calculational proof
7. Mathematical Aspects 7.1 Mathematical aspects in general 7.2 Computational complexity 7.3 Formalised mathematics 7.4 Verifying computer algebra systems 7.5 Abstract algebra 7.6 Analysis	8. Hardware Verification 8.1 Hardware verification in general 8.2 Computer architecture verification 8.3 Clock synchronisation 8.4 Cache-coherence protocols 8.5 Hardware specification 8.6 Hardware synthesis 8.7 Microprocessor verification 8.8 Multiprocessor memory models 8.9 Floating point verification
9. Program Verification 9.1 Program verification in general 9.2 Program extraction and synthesis 9.3 Program refinement 9.4 Program transformation 9.5 Verification condition generation	10. Embedded Languages and Logics 10.1 Embedded languages and logics in general 10.2 Hardware description languages 10.3 Imperative programming languages 10.4 Logic programming languages 10.5 Functional programming languages 10.6 Object-oriented programming languages
11. General Computing Applications 11.1 Process calculi 11.2 Mobility calculi 11.3 Communications protocols 11.4 Security protocols 11.5 Transition systems 11.6 Real-time systems 11.7 Reactive systems	12. Other Areas

You should now be ready to submit your paper to TPHOLs'99.