Participation Call: TPHOLs'96 - Theorem Proving in Higher Order Logics

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

                            CALL FOR PARTICIPATION


        *  If you have Web access, all the following information   *
        *     and more is available in a nicer format from:        *
        *                                                          *
        *        http://www.abo.fi/~jharriso/TPHOLs96.html         *

The 1996 International Conference on Theorem Proving in Higher Order Logics
will be held on 27-30 August 1996 (Tuesday to Friday) in Turku (Abo in Swedish)
in the South-west corner of Finland. Two tutorials are also included, starting
after midday on Monday 26th August.

The conference will be a venue for presentations on the following topics, among
others: advances in interactive theorem proving, proof automation and decision
procedures, applications of mechanized theorem proving, comparison between
different theorem proving approaches, exploiting external tools within theorem
provers and incorporating theorem provers into larger systems.

Previous conferences have been at Cambridge (UK), Aarhus, Davis, Leuven,
Vancouver, Malta and Salt Lake City. This conference is being organized by the
Turku Centre for Computer Science (TUCS) and Abo Akademi University.

  * The third Workshop on Designing Correct Circuits (DCC) will be held from *
  * Monday 2 September to Wednesday 4 September 1996 at Bastad in Southern   *
  * Sweden. This is an excellent opportunity for researchers from outside    *
  * Europe to attend both conferences.                                       *

If you require any further information, please contact the organizing committee
on "orgcom@abo.fi", or any of the members (Joakim von Wright, Jim Grundy or
John Harrison) at the following address:

       Abo Akademi University
       Department of Computer Science
       Lemminkaisenkatu 14A
       20520 Turku



  The 1996 International Conference on Theorem Proving in Higher Order Logics

Monday 26 August

12.00   Registration

12.30   Lunch

14.00   Tutorial: Reflections on aspects of the design of Nuprl and PVS
        Paul Jackson (U. Edinburgh)

15.40   Break

16.00   Tutorial: The Coq proof assistant: principle and practice
        Christine Paulin (ENS Lyon)

18.00   Dinner

*       *       *       *       *       *       *       *

Tuesday 27 August

8.30    Late registration and breakfast

9.30    Conference opens

9.45    Session 1

        A comparison of MDG and HOL for hardware verification
        Sofiene Tahar (U. Montreal), Paul Curzon (U. Cambridge)

        Coq and hardware verification: a case study
        Solange Coupet-Grimal, Line Jakubiec (Lab. Informatique de Marseille)

10.55   Break

11.20   Session 2

        A mechanisation of computability theory in HOL
        Vincent Zammit (U. Kent)

        Using lattice theory in higher order logic
        Linas Laibinis (TUCS, Turku)

12.30   Lunch

14.00   Session 3

        Verification of compiler correctness for the WAM
        Cornelia Pusch (TU Munchen)

        Applying the composition principle to verify a
          micro-kernel operating system
        Heckman, Zhang, Becker, Peticolas, Levitt, Olsson (UC Davis)

15.10   Break

15.40   Session 4

        Proving liveness of fair transition systems
        Holger Busch (Siemens AG, Munchen)

        A modular coding of UNITY in Coq
        Barbara Heyd (INRIA Lorraine), Pierre Cregut (France Telecom)

18.00   Dinner, Volleyball and Sauna

*       *       *       *       *       *       *       *

Wednesday 28 August

8.30    Invited lecture: Set theory, higher order logic or both?
        Mike Gordon (U. Cambridge)

9.30    Break

9.45    Session 5

        Program derivation using the Refinement Calculator
        Michael Butler (U. Southampton), Thomas Langbacka (U. Helsinki)

        A proof tool for reasoning about functional programs
        Graham Collins (U. Glasgow)

10.55   Break

11.20   Session 6

        Function definition in higher-order logic
        Konrad Slind (TU Munchen)

        Five axioms of alpha-conversion
        Andy Gordon (U. Cambridge), Tom Melham (U. Glasgow)

12.30   Lunch

13.30   Session 7

        Implementation issues about the embedding of
          existing high level synthesis algorithms in HOL
        Dirk Eisenbiegler, Christian Blumenroehr, Ramayya Kumar (Karlsruhe)

        Stalmarck's algorithm as a HOL derived rule
        John Harrison (Abo Akademi)

15.00 - 22.00   Excursion

*       *       *       *       *       *       *       *

Thursday 29 August

8.30    Invited lecture: Development of the Mizar Mathematical Library
        Andrzej Trybulec (U. Warsaw, Bialystok)

9.30    Break

9.45    Session 8

        Modeling a hardware synthesis methodology in Isabelle
        David Basin, Stefan Friedrich (MPI, Saarbrucken)

        Improving the result of high-level synthesis using
          interactive transformational design
        Mats Larsson (Volvo, Goteborg)

10.55   Break

11.20   Session 9

        A comparison of HOL and ALF formalizations of a
          categorical coherence theorem
        Sten Agerholm (IFAD), Ilya Beylin (Chalmers), Peter Dybjer (Chalmers)

        Synthetic domain theory in type theory:
          another logic of computable functions
        Bernhard Reus (Ludwig-Maximilians Universitat, Munchen)

12.30   Lunch

14.00   Session 10

        Cryptographic protocol adequacy with HOL: the implementation
        Steven Brackin (Arca Systems, Inc)


            Abstracting signals: the waveform library
            Robert H. Beers, Phillip J. Windley (BYU)

            A proved type inference tool for ML:
              Damas-Milner within Coq (work in progress)
            Catherine Dubois, Valerie Menissier-Morain (U. d'evry)

            Problem solving with tactics
            Hagiya, Tanaka, Yamamoto (U. Tokyo), Nishizaki (Chiba U.)

            Deeply embedding behavioral hardware description languages
            Michael D. Jones, Trent N. Larson, Phillip J. Windley (BYU)

            Using auxiliary knowledge in automating invariant proofs
            Pertti Kellomaki (Tampere U. Technology)

            Derivation of verification rules from operational definitions
            Michael Norrish (U. Cambridge)

            Natural proofs versus programs optimization in the
              Calculus of Inductive Constructions
            Catherine Parent (VERIMAG, France)

            Extending a state transition system with real-time semantics
            Peticolas, Zhang, Becker, Heckman, Levitt, Olsson (UC Davis)

            A HOL model of interlocking systems
            Wai Wong (Hong Kong Baptist U.)

15.30   Break

16.00   Session 11

        A Mizar mode for HOL
        John Harrison (Abo Akademi)

        Higher-order annotated terms for proof search
        Alan Smaill, Ian Green (U. Edinburgh)

19.00   Conference dinner

*       *       *       *       *       *       *       *

Friday 30 August

8.30    Session 12

        Inference rules for programming languages with
          side effects in expressions
        Paul E. Black, Phillip J. Windley (BYU)

        Formal verification of algorithm W
        Dieter Nazareth, Tobias Nipkow (TU Munchen)

9.40    Break

10.00   Session 13

        Elements of mathematical analysis in PVS
        Bruno Dutertre (Royal Holloway, U. London)

        Importing mathematics from HOL into Nuprl
        Doug Howe (Bell Labs)

11.10   Break

11.30   Session 14

        A structure preserving encoding of Z in HOL
        Kolyang (Bremen), Thomas Santen (GMD First), Burkhart Wolff (Bremen)

        Translating specifications in VDM-SL to higher order logic
        Sten Agerholm (IFAD, Denmark)

12.40   Conference closes

12.50   Lunch

14.00   Administrative session



The fee for early registration, on or before Friday 21 June is FIM200. There
are separate fees for accommodation and meals. If, as we expect, you are
staying at the conference venue, Turun Kristillinen Opisto, the cost is FIM200
per person (single) or FIM150 per person (shared), per night. If you prefer to
stay at a central hotel, the corresponding costs will be approximately FIM270
and FIM150. Meals, conference banquet and refreshments for the whole
conference cost an additional FIM876 per person, or FIM705 for guests not
requiring refreshments during the breaks. A more detailed breakdown of the
costs is available on the Web at:


After Friday 21 June, the registration fee rises to FIM250, and after the end
of July, we will be unable to guarantee accommodation at the same price and
standard. You can register via the Web; see:


Alternatively, fill in the following form, and either:

 * Email it to "orgcom@abo.fi"

 * Fax it to any member of the organizing committee on +358 21 265-4732

 * Send it by mail to the organizing committee (see the address above).

By registering for TPHOLs'96 you are agreeing to pay the applicable
registration fee even if you subsequently fail attend the conference. If you
are unable to attend the conference then the organizing committee may waive the
fee if you inform us of your change of plans in a timely manner. However, if
you just fail to show up, we are going to want our money.

 1. Name: ________________________________________________________
    (as you would like it to appear on your name tag)

 2. Affiliation:



  3. Address:




 4. Email: _______________________________________________________

 5. Fax: +________________________________________________________

 6. Phone: +______________________________________________________

 7. Arrival Day:
      [_] Friday   23 August
      [_] Saturday 24 August
      [_] Sunday   25 August
      [_] Monday   26 August
      [_] Tuesday  27 August
    Arrival Time: ________________________________________________
    Arrival Point:
      [_] Turku Airport
      [_] Turku Railway Station
      [_] Turku Bus Station
      [_] Turku Harbor, Silja Terminal
      [_] Turku Harbor, Viking Terminal
      [_] Unknown
 8. Departure Day:
      [_] Thursday 29 August
      [_] Friday   30 August
      [_] Saturday 31 August
      [_] Sunday    1 September
      [_] Monday    2 September

 9. Number of Accompanying Guests: __
      These are people not attending the conference, but for whom
      you would like meals and accommodation arranged.

10. Accommodation is available either at the conference venue,
    Turun Kristillinen Opisto, located a few kilometers from the
    centre of town; or at various centrally located hotels.  We
    expect most people will stay at Turun Kristillinen Opisto.

    Would you like to stay at:
      [_] Turun Kristillinen Opisto
            FIM200 per person, per night single.
            FIM150 per person, per night shared.
      [_] A central hotel
            FIM270 per person, per night single.
            FIM150 per person, per night shared.
      [_] I'll arrange my own accommodation thanks.

    Note that we are unable to guarantee the same prices or
    quality of accommodation for people registering after July.

11. Special Dietary Requirements: ________________________________

12. Special Access Requirements: _________________________________

13. Would you like to share a room? (other than with your guests)
      [_] no
      [_] yes
          With anyone in particular?
            [_] yes: _____________________________________________
            [_] no
                You are:
                  [_] female
                  [_] male
                You would be content to share with a:
                  [_] female
                  [_] male

14. Would you buy a TPHOLs'96 T-shirt if we made one?
      [_] yes, size [_] S [_] M [_] L [_] XL
      [_] no
    T-shirts would be sold at their cost price.

15. The conference registration fee is as follows:
      * FIM200 for early registration (Friday 21 June or earlier).
      * FIM250 for late registration (Saturday 22 June or later).
    Payable in cash (Finnish Markka only) at the Conference.

    In addition to the registration fee, there will be a fee for
    meals and accommodation (details available elsewhere).  You
    can pay for your accommodation and meals at the conference in
    cash (Finnish Markka only), or with the following credit cards
    only: Diner's Club, EuroCard, MasterCard or Visa.

    How will you be paying for your meals and accommodation?
      [_] Cash (Finnish Markka)
      [_] Diner's Club
      [_] EuroCard
      [_] MasterCard
      [_] Visa