[isabelle] [TPHOLs'2008] Business Meeting.

TPHOLs'2008 Business Meeting

August 21, 2008 (3-4pm)

The meeting  started with  Sofiene Tahar presenting  a summary  of the
initial proposal for  TPHOLS2008, a summary of how  things went in the
conference  this year. This  was followed  by a  brief talk  by Tobias
Nipkow about TPHOLs 2009. Matt Kaufman talked then about his ideas for
TPHOLs 2010. After that several issues were discussed including TPHOLs
name change, and  venue for 2011. The meeting  ended with Matt Kaufman
thanking  Sofiene  Tahar, Otmane  Ait  Mohammed  and  Cesar Munoz  for
arranging TPHOLs 2008.

Sofiene started  by showing a  presentation from his  initial proposal
for TPHOLs  2008 given at the  business meeting of  TPHOLs 2007.  Main
features  in   the  proposal  were,  in  commemoration   of  20  years
anniversary:   embedded  tutorials,   invited  talks,   and  satellite
workshops together with regular  contributions. He then summarized the
time  line  from  call  for   papers  for  TPHOLs  2008,  to  abstract
submissions, to  submission of papers,  notice of acceptance  and then
finally some  conference statistics. 45 papers were  submitted from 13
countries.  Sixteen were  accepted as  regular papers,  6  as emerging
trend papers,  and 1 as proof  pearl. The regular  session papers were
archived  in  LNCS  format  where  emerging  trends  proceedings  were
provided to  the participants (hardcopies  and CD ROM). CD  as default
and hardcopy by request (he  reported that 20 copies were enough!). It
was also  promised that the source  code, and slides  of all tutorials
and invited  talks shall be provided  on the conference web  site in a
few days.

While talking about finances Sofiene mentioned that there were several
generous  sponsors  which  made  this event  possible,  they  included
Concordia University, the Faculty of Engineering and Computer Science,
INTEL, RESMIQ,  and NIA. All the  expenses are expected to  be met and
there  may be some  money left  over! Special  rates were  provided to
students  attending  the  conference.  There  was a  plan  to  provide
bursaries  to   some  students  attending  the   conference  but  that
unfortunately  could not  be accomplished.   Overall, this  year there
were 39 regular attendees, 23 students  + 6 from Concordia, a total of

Tobias then talked  about TPHOLS 2009. The TPHOLs  conference web site
is "http://tphols.in.tum.de";.  In his presentation,  he showed several
pictures of the university  campus and the computer science department
building, and  the "slide"  from the third  floor of the  building. He
suggested two possible  dates for the conference, either  third or the
last  week   of  August  of   2009  with  first  preference   for  the
latter. Tobias also mentioned that he has checked web sites of several
other conference such as CADE, FMCAD,  CAV, etc. to make sure there is
no date conflicts. The conference  format will be the same as previous
year, spread over four days  and consisting of invited papers, regular
contributions, emerging trends, and a  workshop on the last day of the
conference,  The  organizers of  TPHOLs  are  Tobias Nipkow,  Makarius
Wenzel, Stefan Berghofer, and Christian Urban.

The 22nd  TPHOLs will take place  in the computer  science building of
the  Technische   Universitat  Munchen.  The  venue  is   out  of  the
city.  There are no  hotels on  campus. Nearest  hotel is  about 20-25
minutes walk away. One can take the subway to Munich which takes about
25 minutes. There one can find a range of prices for hotels. There are
direct flights from several metropolitan cities to Munich, e.g. Paris,
London, Nice, Montreal,  Chicago. The excursion will be  probably be a
visit to museum followed by a  city tour. Archival format will be LNCS
and support for the invited  speakers will be provided. The organizers
will be looking for sources of  support but the cost in Munich may not
be  as low  Montreal which  was  truly exceptional,  as elaborated  by

Matt  talked  about  TPHOLs/ITP  in  2010.  ITP  (Interactive  theorem
Proving)  2010 will  be held  in Edinburgh  as part  of FLoC  2010. He
briefly described the history  of TPHOLs name change. Initially TPHOLs
wanted to be part of FLoC, but  FLoC said no. Then an idea was floated
that  if TPHOLs  and ACL2  can join  together, then  they can  reach a
critical mass needed to be part of FLOC (Approximately 30 participants
from ACL2, and about 60 participants from TPHOLs community)

For 2010, the idea is to have one day tutorial, two parallel sessions,
one for ACL2 community and one  for the HOL community. Through show of
hands about  20 to  25 showed  interest in attending  a full  day ACL2
tutorial.  There were  about 65 people present in  the conference room
at the time of the show of hand vote.

This  was followed  by open  discussion of  several issues.  The first
issue  discussed was  the change  of name  of TPHOLs  to  ITP starting
2010. Matt lead  the discussion. He asked  if this is a  good idea? He
also mentioned that the steering committee seemed to like it. This was
followed by  a short discussion, mostly  in favor of  the name change,
with some against the change of  name arguing the loss of the "TPHOLs"
icon.  Burkhart  Wolf, John Mathews, Peter Homier,  Matt Kaufman, Yves
Bertot, David  Lester, Cameron  Freer and several  others participated
int  the discussion.  Some of  the  comments included  "it's a  better
name", "we  deal with problems which  are much harder  to handle", "we
bring human insight into the automated reasoning", "Its just evolution
of the name", "it will help draw more representation from industry and
the  mathematics community",  "the number  21st  gives us  an aura  of
respectability so we should not  reset the number of the conference to
one", "FLOC is a good venue to start a new name".

Sofiene suggested that since not all in the HOL community are present,
we should ask for feedback  regarding the name change through email. A
question  was asked  who should  lead this  effort, and  Tobias kindly
accepted to do it.

A question  was asked about what's  the plan after  FLoC 2010. Sofiene
mentioned that  Elsa Gunter showed interest in  holding the conference
at University of Urbana Champaign in 2011.

It was mentioned  that it has been a tradition  to hold the conference
in Europe one year and in  a country outside Europe the following year
(or in broader  sense change continent every year).  Issues about visa
to USA were  discussed. There was a mention  of avoiding countries who
have  unreasonable   policies  regarding  immigration   and  therefore
difficulty for  travel. Some  countries will not  give visas  and some
have a lot of paperwork that needs to be done to get a visa.

Finally,  Matt thanked Sofiene  Tahar, Otmane  Ait Mohammed  and Cesar
Munoz for arranging the conference this year.  One of the participants
mentioned that he  registered late and was not able  to find the exact
location from  the conference web site. Sofiene  replied that detailed
information about  the conference  was to sent  to all  the registered
participants a few days before the conference via email.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.