Programming Concepts and Methods PROCOMET ’98

1. Front Matter

   Pages i-ix

   PDF

2. Extended static checking

   • K. R. M. Leino

   Pages 1-1

3. From Lattices to Practical Formal Hardware Verification

   • C. Seger

   Pages 3-3

4. Programming with Tabling in XSB

   • D. S. Warren

   Pages 5-5

5. Verifying Electronic Control Units — today and tomorrow

   • W. Damm

   Pages 7-7

6. Teaching Calculational Logic

   • D. Gries

   Pages 9-9

7. Types for Trees

   • E. Barbanera, M. Dezani-Ciancaglini, F. J. de Vries

   Pages 11-29

8. Structures for lazy semantics

   • O. Bastonero, A. Pravato, S. Ronchi della Rocca

   Pages 30-48

9. A proof theory of asynchronously communicating sequential processes

   • F. S. de Boer, N. Francez, M. van Hulst, F. A. Stomp

   Pages 49-67

10. Bisimulations in the Join-Calculus

    • M. Boreale, C. Fournet, C. Laneve

    Pages 68-86

11. Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols

    • E. M. Clarke, S. Jha, W. Marrero

    Pages 87-106

12. Programming Language Semantics in Foundational Type Theory

    • K. Crary

    Pages 107-125

13. An Algebraic Approach to the Specification of Stochastic Systems (Extended Abstract)

    • P. R. D’Argenio, J.-P. Katoen, E. Brinksma

    Pages 126-147

14. Refinement types for specification

    • E. Denney

    Pages 148-166

15. An extension of the program derivation format

    • A. J. M. van Gasteren, A. Bijlsma

    Pages 167-185

16. Deadlines are termination

    • I. J. Hayes, M. Utting

    Pages 186-204

17. The design of a linearization of a concurrent data object

    • W. H. Hesselink

    Pages 205-224

18. Final semantics for the π-calculus

    • F. Honsell, M. Lenisa, U. Montanari, M. Pistore

    Pages 225-243

19. Comparing CTL and PCTL on Labeled Markov Chains

    • M. R. A. Huth, M. Z. Kwiatkowska

    Pages 244-262

20. Reactive Functional Programming

    • R. B. Kieburtz

    Pages 263-284

This book constitutes the Proceedings of the IFIP Working Conference PRO­ COMET'98, held 8-12 June 1998 at Shelter Island, N.Y. The conference is organized by the t'wo IFIP TC 2 Working Groups 2.2 Formal Description of Programming Concepts and 2.3 Programming Methodology. WG2.2 and WG2.3 have been organizing these conferences every four years for over twenty years. The aim of such Working Conferences organized by IFIP Working Groups is to bring together leading scientists in a given area of computer science. Participation is by invitation only. As a result, these conferences distinguish themselves from other meetings by extensive and competent technical discus­ sions. PROCOMET stands for Programming Concepts and Methods, indicating that the area of discussion for the conference is the formal description of pro­ gramming concepts and methods, their tool support, and their applications. At PROCOMET working conferences, papers are presented from this whole area, reflecting the interest of the individuals in WG2.2 and WG2.3.

• Mathematica
• algorithms
• design
• formal specification
• functional programming
• object
• programming
• programming language
• security
• semantics
• simulation
• software
• software engineering
• structured analysis
• verification

• Dept. of Computer Science, Cornell University, Ithaca, USA

  David Gries

• Institute of Computer Science & Applied Mathematics, Christian-Albrechts-University of Kiel, Germany

  Willem-Paul Roever

Policies and ethics