[Prev][Next][Index][Thread]
Participation Call: TPHOLs'96 - Theorem Proving in Higher Order Logics
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
CALL FOR PARTICIPATION
THE 1996 INTERNATIONAL CONFERENCE ON THEOREM PROVING IN HIGHER ORDER LOGICS
************************************************************
* 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
FINLAND
============================================================================
PROGRAMME
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)
POSTER SESSION
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
============================================================================
REGISTRATION
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:
http://www.abo.fi/~jharriso/cost.html
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:
http://www.abo.fi/~jharriso/webform.html
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