IMPORTANT: Abstract deadline: Tuesday, February 1 (firm) Call for Papers
The International Conference on Interactive Theorem Proving (ITP 2022) will take place on August 7-10, 2022 in Haifa, Israel. It will be part of FLoC 2022 https://floc2022.org/<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffloc2022.org%2F&data=04%7C01%7Cleonardo%40microsoft.com%7C6cf2fc8ac9f945591de208d9cfd6fd6b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637769346069003688%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=ntLZtl4c4%2FaxQ2U1MAvSjH7MuLGL2zz08pIJo3%2BuCqI%3D&reserved=0>. The FLoC organizing committee will make all efforts possible to ensure everyone can attend in person. However, they are very much aware that there might be members of the community who cannot travel to Israel. In cases where travel is not possible, they will ensure people can participate remotely. The ITP conference series is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics. This will be the 13th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988. Paper Submission ITP welcomes submissions describing original research on all aspects of interactive theorem proving and its applications. Suggested topics include, but are not limited to, the following: formalizations of computational models improvements in theorem prover technology formalizations of mathematics integration with automated provers and other symbolic tools verification of security algorithms industrial applications of interactive theorem provers formal aspects of hardware and software user interfaces for interactive theorem provers use of theorem provers in education concise and elegant worked examples of formalizations (proof pearls) Submissions will undergo single-blind peer review. They should be no more than 16 pages in length, excluding bibliographic references in LIPIcs format (for detailed instructions for authors on document preparation see: https://submission.dagstuhl.de/series/details/5#author<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fsubmission.dagstuhl.de%2Fseries%2Fdetails%2F5%23author&data=04%7C01%7Cleonardo%40microsoft.com%7C6cf2fc8ac9f945591de208d9cfd6fd6b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637769346069013644%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=di2By5rOR3E28HBkOFF1mXqHSZY3vlSF6txVJP510Jw%3D&reserved=0>). The papers are to be submitted in PDF format via EasyChair via the following link: https://easychair.org/conferences/?conf=itp2022<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Feasychair.org%2Fconferences%2F%3Fconf%3Ditp2022&data=04%7C01%7Cleonardo%40microsoft.com%7C6cf2fc8ac9f945591de208d9cfd6fd6b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637769346069018619%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=LHTEsvF7qUzWWkwv16lK5lP%2FL%2B13wzCmD8dX92X0Oz4%3D&reserved=0> We also welcome short papers, which can be used to describe interesting work that is still ongoing and not fully mature ("rough diamonds"). Such a preliminary report is limited to 6 pages and may consist of an extended abstract. Each of these papers should bear the phrase “(short paper)” beneath the title. Accepted submissions in this category will be published in the main proceedings and will be presented as short talks. All submissions are expected to be accompanied by verifiable evidence of a suitable implementation, such as the source files of a formalization for the proof assistant used. Important Dates Abstract deadline: Tuesday, February 1 (firm) Paper submission deadline: Tuesday, February 8 (firm) Author Notification: Wednesday, March 30 Camera-ready copy due: Wednesday, April 27 Conference: August 7-10 Invited Speakers Amy Felty<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.site.uottawa.ca%2F~afelty%2F&data=04%7C01%7Cleonardo%40microsoft.com%7C6cf2fc8ac9f945591de208d9cfd6fd6b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637769346069023602%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=fUvedhgMsSv8KCNF2ZurFxOeCgx6uY3L2%2Fu%2B8%2Bx1msk%3D&reserved=0>, School of Electrical Engineering and Computer Science (EECS), University of Ottawa Bohua Zhan<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Flcs.ios.ac.cn%2F~bzhan%2F&data=04%7C01%7Cleonardo%40microsoft.com%7C6cf2fc8ac9f945591de208d9cfd6fd6b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637769346069028577%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=C3egD%2FT8pjRKW5sYFER6IpdENwoR5HXjfLsRaKanl6c%3D&reserved=0>, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Conference Website https://itpconference.github.io/ITP22/<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fitpconference.github.io%2FITP22%2F&data=04%7C01%7Cleonardo%40microsoft.com%7C6cf2fc8ac9f945591de208d9cfd6fd6b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637769346069033560%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=jk6jTpWRb4o7Ov7sxZHESnyBkSQXtLfvQMZolXsbsDQ%3D&reserved=0> Publication Details The conference proceedings will be published in the LIPIcs series (“Leibniz International Proceedings in Informatics”). This was chosen in large part because of its commitment to free and open access to all papers. For more information on the series, see https://www.dagstuhl.de/en/publications/lipics<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.dagstuhl.de%2Fen%2Fpublications%2Flipics&data=04%7C01%7Cleonardo%40microsoft.com%7C6cf2fc8ac9f945591de208d9cfd6fd6b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637769346069038533%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=78OtUQ3d0A3n0QFaz75kfS1k0uO03AWVdGZSzsUfkkI%3D&reserved=0> and for more detailed instructions for authors on document preparation: https://submission.dagstuhl.de/series/details/5#author<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fsubmission.dagstuhl.de%2Fseries%2Fdetails%2F5%23author&data=04%7C01%7Cleonardo%40microsoft.com%7C6cf2fc8ac9f945591de208d9cfd6fd6b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637769346069043511%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=3dgTNNuSC%2FSj%2BrRkStYNFPS%2FKzydwm5Y790abt%2Bb%2Fek%3D&reserved=0> -- You received this message because you are subscribed to the Google Groups "lean-user" group. To unsubscribe from this group and stop receiving emails from it, send an email to lean-user+unsubscr...@googlegroups.com<mailto:lean-user+unsubscr...@googlegroups.com>. To view this discussion on the web visit https://groups.google.com/d/msgid/lean-user/SJ0PR21MB1339FE7051327FE3ACD72EA9D14A9%40SJ0PR21MB1339.namprd21.prod.outlook.com<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgroups.google.com%2Fd%2Fmsgid%2Flean-user%2FSJ0PR21MB1339FE7051327FE3ACD72EA9D14A9%2540SJ0PR21MB1339.namprd21.prod.outlook.com%3Futm_medium%3Demail%26utm_source%3Dfooter&data=04%7C01%7Cleonardo%40microsoft.com%7C6cf2fc8ac9f945591de208d9cfd6fd6b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637769346069048492%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=zo7UK6sSRTTMEN4SZJffrgPOcMMntPFu61Kh2wgnL7o%3D&reserved=0>.
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
