Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.



TPHOLs'96 Early Registration Closing for Theorem Proving Conf.
Posted:
Jun 20, 1996 3:40 AM


Please note that the Friday 21 June is the closing date for early registration for TPHOLs'96. After that, the cost of attending the conference will rise slightly. You need send no money to register, but you must register now if you wish to pay the lower fee on arrival at the conferecnce.
CALL FOR PARTICIPATION
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 2730 August 1996 (Tuesday to Friday) in Turku (Abo in Swedish) in the Southwest 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
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 CoupetGrimal, 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 microkernel 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 higherorder logic Konrad Slind (TU Munchen)
Five axioms of alphaconversion 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 highlevel 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 (LudwigMaximilians 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: DamasMilner within Coq (work in progress) Catherine Dubois, Valerie MenissierMorain (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 realtime 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)
Higherorder 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 VDMSL 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 2654732
* 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 Tshirt if we made one? [_] yes, size [_] S [_] M [_] L [_] XL [_] no Tshirts 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
From jgrundy Thu Jun 20 10:38:38 1996 Sender: jgrundy@bruce.abo.fi (Jim Grundy INF) Newsgroups: alt.uu.math.misc,comp.object.logic, >From: jgrundy@news.abo.fi (Jim Grundy INF) ReplyTo: Jim Grundy <jim.grundy@abo.fi> comp.specification.larch, comp.specification.misc, comp.specification.z, comp.theory, fj.comp.theory, nordunet.sci.math, nordunet.sci.math.euro, sci.logic, sci.math, sci.math.symbolic Distribution: world FollowupTo: Organization: Abo Akademi >Subject: TPHOLs'96 Early Registration Closing for Theorem Proving Conf. Keywords:
Please note that the Friday 21 June is the closing date for early registration for TPHOLs'96. After that, the cost of attending the conference will rise slightly. You need send no money to register, but you must register now if you wish to pay the lower fee on arrival at the conferecnce.
CALL FOR PARTICIPATION
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 2730 August 1996 (Tuesday to Friday) in Turku (Abo in Swedish) in the Southwest 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
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 CoupetGrimal, 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 microkernel 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 higherorder logic Konrad Slind (TU Munchen)
Five axioms of alphaconversion 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 highlevel 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 (LudwigMaximilians 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: DamasMilner within Coq (work in progress) Catherine Dubois, Valerie MenissierMorain (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 realtime 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)
Higherorder 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 VDMSL 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 2654732
* 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 Tshirt if we made one? [_] yes, size [_] S [_] M [_] L [_] XL [_] no Tshirts 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



