Email Gateway (Aug 18 2022 at 12:20): Email Gateway (Aug 18 2022 at 12:20):From: Otmane Ait Mohamed <ait@encs.concordia.ca>
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
68.
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
Tobias.
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.
Last updated: May 03 2024 at 08:18 UTC