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.