[TYPES/announce] ITP 2024, Interactive Theorem Proving: Last Call For Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] https://urldefense.com/v3/__https://www.viam.science.tsu.ge/itp2024/__;!!IBzWLUs!QkIg5Y1zVp8-0bRa8jX9BxkqzYyFuaV18Jj2jBWGRF4JZ2MuzymsFmUFyY3M6-7QQRrCuzme37NkPjsqy6wqyR3bfsMUDO7WDo6M$ The international conference on Interactive Theorem Proving (ITP 2024) will take place on September 9-14, 2024 in Tbilisi, Georgia. It is planned as a hybrid meeting. It will mostly be a face-to-face (physical) meeting but facilities will be provided for remote presentation and remote attendance. 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 15th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988. Paper Submission The main proceedings will be published as part of the Leibniz International Proceedings in Informatics (LIPIcs). 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 interactive 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 specification and verification 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. Regular papers must: - be no more than 16 pages in length excluding bibliographic references - not include an appendix; and - be in LIPIcs format. For detailed instructions for authors on document preparation see: https://urldefense.com/v3/__https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/__;!!IBzWLUs!QkIg5Y1zVp8-0bRa8jX9BxkqzYyFuaV18Jj2jBWGRF4JZ2MuzymsFmUFyY3M6-7QQRrCuzme37NkPjsqy6wqyR3bfsMUDImjNnLH$ We also welcome short papers, which can be used to describe interesting work that is still ongoing and not fully mature. Such a preliminary report is limited to 6 pages and may consist of an extended abstract. Each of these papers should have the phrase "Short paper" as a subtitle. Accepted submissions in this category will be published in the main proceedings and will be presented as short talks. The papers are to be submitted via EasyChair via the following link: https://urldefense.com/v3/__https://easychair.org/conferences/?conf=itp2024__;!!IBzWLUs!QkIg5Y1zVp8-0bRa8jX9BxkqzYyFuaV18Jj2jBWGRF4JZ2MuzymsFmUFyY3M6-7QQRrCuzme37NkPjsqy6wqyR3bfsMUDDv57Jvy$ 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 (AoE) Abstract submission deadline: March 11, 2024 Paper submission deadline: March 18, 2024 Author notification: May 20, 2024 Camera-ready copy due: June 10, 2024 Conference: September 9-14, 2024
[TYPES/announce] ITP 2024 : Second call for papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] https://urldefense.com/v3/__https://www.viam.science.tsu.ge/itp2024/__;!!IBzWLUs!XA2hswRuv_iKtrd_e2lK2OPaCiADah9YhOuyyp-R5nY4JqcFPbPesWMCwxarP1RKVs3SGLoZpqkiD9Rne-LjXeMuANAYFBCawu7E$ The international conference on Interactive Theorem Proving (ITP 2024) will take place on September 9-14, 2024 in Tbilisi, Georgia. It is planned as a hybrid meeting. It will mostly be a face-to-face (physical) meeting but facilities will be provided for remote presentation and remote attendance. 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 15th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988. Paper Submission The main proceedings will be published as part of the Leibniz International Proceedings in Informatics (LIPIcs). 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 interactive 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 specification and verification 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. Regular papers must: - be no more than 16 pages in length excluding bibliographic references - not include an appendix; and - be in LIPIcs format. For detailed instructions for authors on document preparation see: https://urldefense.com/v3/__https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/__;!!IBzWLUs!XA2hswRuv_iKtrd_e2lK2OPaCiADah9YhOuyyp-R5nY4JqcFPbPesWMCwxarP1RKVs3SGLoZpqkiD9Rne-LjXeMuANAYFAY_GXKv$ We also welcome short papers, which can be used to describe interesting work that is still ongoing and not fully mature. Such a preliminary report is limited to 6 pages and may consist of an extended abstract. Each of these papers should have the phrase "Short paper" as a subtitle. Accepted submissions in this category will be published in the main proceedings and will be presented as short talks. The papers are to be submitted via EasyChair via the following link: https://urldefense.com/v3/__https://easychair.org/conferences/?conf=itp2024__;!!IBzWLUs!XA2hswRuv_iKtrd_e2lK2OPaCiADah9YhOuyyp-R5nY4JqcFPbPesWMCwxarP1RKVs3SGLoZpqkiD9Rne-LjXeMuANAYFD3qOlOz$ 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 (AoE) Abstract submission deadline: March 11, 2024 Paper submission deadline: March 18, 2024 Author notification: May 20, 2024 Camera-ready copy due: June 10, 2024 Conference: September 9-14, 2024
[TYPES/announce] ITP 2024: First Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] ITP 2023: First Call for Papers https://urldefense.com/v3/__https://www.viam.science.tsu.ge/itp2024/__;!!IBzWLUs!SmNA2vGo8kcckWwGwl-tqWifExJyBZn101peaOV761uys1E51lZjJ8PtBDmcCexLNqRZLVJnzbCF9SbddykHTrlx4OSXH8oHETW6$ The international conference on Interactive Theorem Proving (ITP 2024) will take place on September 9-14, 2024 in Tbilisi, Georgia. It is planned as a face-to-face (physical) meeting. 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 15th 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. Regular papers should be no more than 16 pages in length excluding bibliographic references in LIPIcs format, and they should not include an appendix. For detailed instructions for authors on document preparation see: https://urldefense.com/v3/__https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/__;!!IBzWLUs!SmNA2vGo8kcckWwGwl-tqWifExJyBZn101peaOV761uys1E51lZjJ8PtBDmcCexLNqRZLVJnzbCF9SbddykHTrlx4OSXH_vICDGz$ We also welcome short papers, which can be used to describe interesting work that is still ongoing and not fully mature. Such a preliminary report is limited to 6 pages and may consist of an extended abstract. Each of these papers should have the phrase "Short paper" as a subtitle. Accepted submissions in this category will be published in the main proceedings and will be presented as short talks. The papers are to be submitted via EasyChair via the following link: https://urldefense.com/v3/__https://easychair.org/conferences/?conf=itp2024__;!!IBzWLUs!SmNA2vGo8kcckWwGwl-tqWifExJyBZn101peaOV761uys1E51lZjJ8PtBDmcCexLNqRZLVJnzbCF9SbddykHTrlx4OSXH-NBF73p$ 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 (AoE) Abstract submission deadline: March 11, 2024 Paper submission deadline: March 18, 2024 Author notification: May 20, 2024 Camera-ready copy due: June 10, 2024 Conference: September 9-14, 2024
[TYPES/announce] Deadline Extension: CfP 2023 Coq workshop, May 30th
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] IMPORTANT: We are extending the deadline for submission to the Coq workshop to May 30th, AoE (Anywhere on Earth). We are pleased to invite you to submit presentation proposals for the Coq Workshop 2023, which will be held in Białystok, Poland on July 31 , 2023, as a satellite to the ITP conference. [ https://urldefense.com/v3/__https://coq-workshop.gitlab.io/2023/__;!!IBzWLUs!WjQBQWluZJpzuT5ei-XE1fsJdhlTsrWI-SQo2VEYdYxTpLT9ug6gtCojMRgaC5UjEF9by7SUtBOPFLQ-S8yPJ4y7FD0deI-5Qbhg$ | https://urldefense.com/v3/__https://coq-workshop.gitlab.io/2023/__;!!IBzWLUs!WjQBQWluZJpzuT5ei-XE1fsJdhlTsrWI-SQo2VEYdYxTpLT9ug6gtCojMRgaC5UjEF9by7SUtBOPFLQ-S8yPJ4y7FD0deI-5Qbhg$ ] The Coq Workshop 2023 is the 14th installment of the Coq Workshop series. The workshop brings together users, contributors, and developers of the Coq proof assistant. The Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, rather than serving as a venue for traditional research papers, the workshop is organized around informal presentations and discussions, supplemented with invited talks. Important dates: May 30 , 2023 (AoE): Deadline for submission of presentation proposals June 15 , 2023: Notification to authors July 31 , 2023: Workshop Submission instructions: Authors should submit presentation proposals as extended abstracts through EasyChair. Relevant subject matter includes but is not limited to: Language or tactic features for Coq Theory and implementation of the Calculus of Inductive Constructions Applications of Coq and experience reports on Coq use in education and industry Tools and platforms built on Coq Plugins and libraries for Coq Interfacing with Coq Formalization tricks and Coq pearls Submission format: Presentation proposals should be no more than 2 pages in length including bibliographic references, and should use the EasyChair style with the fullpage package. All submissions must be in PDF format. Program committee: Nada Amin (Harvard) Jesper Bengtson (IT-University of Copenhagen) Yves Bertot (Inria) [chair] Ana Borges (University of Barcelona) Chantal Keller (LMF, Université Paris-Saclay) Pierre Roux (ONERA, Toulouse) Takafumi Saikawa (Nagoya University) Enrico Tassi (Inria) [chair] Organizers and contact: Enrico Tassi and Yves Bertot ( coq2...@easychair.org )
[TYPES/announce] 2nd Call for presentations: 2023 Coq workshop
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are pleased to invite you to submit presentation proposals for the Coq Workshop 2023, which will be held in Białystok, Poland on July 31, 2023, as a satellite to the ITP conference. https://urldefense.com/v3/__https://coq-workshop.gitlab.io/2023/__;!!IBzWLUs!X_sYFMo_a1qe2a9T3xFecgAioGJwsNC2QtmKfb5RsuE0_sGgs3pl33kApYuOGqAAiph_VR8s9U2jYpMu-rGMwxDwaBYP0a8rugpA$ The Coq Workshop 2023 is the 14th installment of the Coq Workshop series. The workshop brings together users, contributors, and developers of the Coq proof assistant. The Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software, piece of software based on type theory and its associated ecosystem of libraries and tools. Thus, rather than serving as a venue for traditional research papers, the workshop is organized around informal presentations and discussions, supplemented with invited talks. Important dates: May 26, 2023 (AoE): Deadline for submission of presentation proposals June 15, 2023: Notification to authors July 31, 2023: Workshop Submission instructions: Authors should submit presentation proposals as extended abstracts through EasyChair. Relevant subject matter includes but is not limited to: Language or tactic features for Coq Theory and implementation of the Calculus of Inductive Constructions Applications of Coq and experience reports on Coq use in education and industry Tools and platforms built on Coq Plugins and libraries for Coq Interfacing with Coq Formalization tricks and Coq pearls Submission format: Presentation proposals should be no more than 2 pages in length including bibliographic references, and should use the EasyChair style with the fullpage package. All submissions must be in PDF format. Program committee: Nada Amin (Harvard) Jesper Bengtson (IT-University of Copenhagen) Yves Bertot (Inria) [chair] Ana Borges (University of Barcelona) Chantal Keller (LMF, Université Paris-Saclay) Pierre Roux (ONERA, Toulouse) Takafumi Saikawa (Nagoya University) Enrico Tassi (Inria) [chair] Organizers and contact: Enrico Tassi and Yves Bertot (coq2...@easychair.org)
[TYPES/announce] 2023 Coq workshop call for presentations
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are pleased to invite you to submit presentation proposals for the Coq Workshop 2023, which will be held in Białystok, Poland on July 31, 2023, as a satellite to the ITP conference. https://urldefense.com/v3/__https://coq-workshop.gitlab.io/2023/__;!!IBzWLUs!TZkbypr524bNFhzSsi53DuD-88GPUOqG1NslSOq6ZY1OCOgFEEzZ9PfI6C3KU823ebpIC7QmA78QyMTCdI5stk-GQk9hXCEsqukt$ The Coq Workshop 2023 is the 14th installment of the Coq Workshop series. The workshop brings together users, contributors, and developers of the Coq proof assistant. The Coq Workshop focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software, piece of software based on type theory and its associated ecosystem of libraries and tools. Thus, rather than serving as a venue for traditional research papers, the workshop is organized around informal presentations and discussions, supplemented with invited talks. Important dates: May 26, 2023 (AoE): Deadline for submission of presentation proposals June 15, 2023: Notification to authors July 31, 2023: Workshop Submission instructions: Authors should submit presentation proposals as extended abstracts through EasyChair. Relevant subject matter includes but is not limited to: Language or tactic features for Coq Theory and implementation of the Calculus of Inductive Constructions Applications of Coq and experience reports on Coq use in education and industry Tools and platforms built on Coq Plugins and libraries for Coq Interfacing with Coq Formalization tricks and Coq pearls Submission format: Presentation proposals should be no more than 2 pages in length including bibliographic references, and should use the EasyChair style with the fullpage package. All submissions must be in PDF format. Program committee: Nada Amin (Harvard) Jesper Bengtson (IT-University of Copenhagen) Yves Bertot (Inria) [chair] Ana Borges (University of Barcelona) Chantal Keller (LMF, Université Paris-Saclay) Pierre Roux (ONERA, Toulouse) Takafumi Saikawa (Nagoya University) Enrico Tassi (Inria) [chair] Organizers and contact: Enrico Tassi and Yves Bertot (coq2...@easychair.org)
[TYPES/announce] Introductory School on Coq, January 22 -- January 26 2017, Sophia Antipolis, France
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] This is an announcement for a one-week intensive course on Coq given at Inria Sophia Antipolis "Software Verification and computer proof" January 22 -- january 26, 2018 Inria Sophia Antipolis https://team.inria.fr/marelle/en/coq-winter-school-2018/ This course is an introductory course intended for students in computer science who have very little knowledge of functional programming and no knowledge of computer proof. The background in mathematics will also be elementary (basically, you are required to know how to perform a division on a sheet of paper). At the end of the week, we expect that students will know how to write little programs (for instance number or list manipulations), write specifications about programs (for instance that a sorting algorithm does not loose data), and perform the proof that programs satisfy specifications. If you, one of your students, or one of your colleagues wishes to learn about Coq from scratch, this may be the right event for you. Registration is free but mandatory and every participant is responsible for their own accommodation, but we can provide some help finding affordable solutions. You can register by sending a mail to Nathalie Bellesso and Yves Bertot ( firstname.n...@inria.fr ).
[TYPES/announce] Two schools on Coq : (Nov 28, 2016) and (Jan 2017), Sophia Antipolis, France
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Marelle team at Inria in Sophia Antipolis is organizing two schools on Coq. 1/ A one week advanced school on Coq and Ssreflect === ADVANCED SOFTWARE VERIFICATION AND COMPUTER PROOF in Sophia-Antipolis (Nice) from Monday November 28th, 2016 to Friday December 2nd. The school will be in English and will target master students with already basic knowledge of Coq. The course will introduce formalization techniques based on the SSReflect proof language and the Mathematical Components library. All relevant data is at: https://team.inria.fr/marelle/advanced-coq-winter-school-2016-2017/ -- Cyril Cohen, Laurence Rideau, Enrico Tassi and Laurent Thery 2/ A one week introductory course === PROGRAMMING, SPECIFYING, AND PROVING WITH THE COQ SYSTEM January 30 -- February 3, 2017 Inria Sophia Antipolis https://team.inria.fr/marelle/coq-winter-school-2017/ This course is an introductory course intended for students in computer science who have very little knowledge of functional programming and no knowledge of computer proof. The background in mathematics will also be elementary (basically, you are required to know how to perform a division on a sheet of paper). At the end of the week, we expect that students will know how to write little programs (for instance number or list manipulations), write specifications about programs (for instance that a sorting algorithm does not loose data), and perform the proof that programs satisfy specifications. If you, one of your students, or one of your colleague wishes to learn about Coq from scratch, this may be the right event for you. Registration is free but mandatory and every participant is responsible for their own accommodation, but we can provide some help finding affordable solutions. You can register by sending a mail to Nathalie Bellesso and Yves Bertot ( firstname.n...@inria.fr ).
[TYPES/announce] CfPart: School on Formalization of Mathematics (March 12-16, 2012, Sophia Antipolis, France)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] International Spring School on FORMALIZATION OF MATHEMATICS Sophia Antipolis, France March 12-16, 2012 http://www-sop.inria.fr/manifestations/MapSpringSchool/ Application deadline: February 27th, 2012 Overview and topics A growing population of mathematicians, computer scientists, and engineers use computers to construct and verify proofs of mathematical results. Among the various approaches to this activity, a fruitful one relies on interactive theorem proving. When following this approach, researchers have to use the formal language of a theorem prover to encode their mathematical knowledge and the proofs they want to scrutinize. The mathematical knowledge often contains two parts: a static part describing structures and a dynamic part describing algorithms. Then proofs are made in a style that is inspired from usual mathematical practice but often differs enough that it requires some training. A key ingredient for the mathematical practitioner is the amount of mathematical knowledge that is already available in the system's library. The Coq system is an interactive theorem prover based on Type Theory. It was recently used to study the proofs of advanced mathematical results. In particular, it was used to provide a mechanically verified proof of the four-color theorem and it is now being used in a long term effort, called Mathematical Components to verify results in group theory, with a specific focus on the odd order theorem, also known as the Feit-Thompson theorem. These two examples rely on a structured library that covers various aspects of finite set theory, group theory, arithmetic, and algebra. The aim of this school is to give mathematicians and mathematically inclined researchers the keys to the Coq system and the Mathematical Components library. The topics covered are: Formal proof techniques Structuring libraries Encoding of common mathematical structures Formal description of algorithms An overview of advanced projects: * The odd order theorem * Constructive algebraic topology * Kepler's conjecture, * Computational analysis, * Foundational investigations. The school's contents will be organized as a balanced schedule between lectures and laboratory sessions where participants will be invited to work on their own computer and try their hands on a progressive collection of exercises. Speakers The current list of speakers is: Georges Gonthier (Microsoft Research) Thomas C. Hales (University of Pittsburgh) Julio Rubio (Universidad de La Rioja) Bas Spitters (Radboud Universiteit, Nijmegen) Vladimir Voevodsky (Institute for advanced study, Princeton) Yves Bertot (Inria) Assia Mahboubi (Inria) Laurence Rideau (Inria) Enrico Tassi (MSR-Inria common laboratory) Laurent Théry (Inria) Registration The registration fee is 320 Euros. A registration form is available on the web site http://www-sop.inria.fr/manifestations/MapSpringSchool/ Location The school will take place at Inria's Sophia Antipolis research center. This center is located 20 mn by bus from the city Antibes on the Mediterranean sea, nearby Nice's international airport, with a variety of hotels at a walking distance. Advice for accomodation is provided on the web page.
[TYPES/announce] [Cfp] Coq Workshop, Edinburgh, July 9, Program and call for participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear Colleague, Please consider attending the Federated Logic Conference (FLoC) and especially the Coq Workshop (Coq-2) Edinburgh, July 9th, 2010 The early registration deadline is May 17th. http://www.floc-conference.org http://coq.inria.fr/coq-workshop/2010 The Coq workshop will bring together Coq users, developers and contributors. It will be organized from submitted and refereed presentations and more informal presentations. Please register and come participate in the discussions, even if you do not wish to submit any talks. The workshop organizers PROGRAM FOR THE COQ WORKSHOP Inductive Proof Automation for Coq by Sean Wilson, Jacques Fleuriot and Alan Smaill Heq: A Coq library for Heterogeneous Equality by Chung-Kil Hur Proof Trick: small Inversions by Jean-François Monin Strengthening the inversion Tactic in Coq by anne mulhern Mixed induction-coinduction at work for Coq by Keiko Nakata and Tarmo Uustalu Certification of a chain for deductive program verification by Paolo Herms Invited talk (title to be announced later) by Hugo Herbelin Rewriting Modulo Associativity and Commutativity by Thomas Braibant and Damien Pous Developing the algebraic hierarchy with type classes in Coq by Bas Spitters, Eelis van der Weegen Experience of interfacing Coq+SSReflect and GAP by Vladimir Komendantsky, Alexander Konovalov and Steve Linton Root isolation for one-variable polynomials by Yves Bertot and Assia Mahboubi
[TYPES/announce] Coq-Workshop: Call for informal presentations (updated information)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Coq Workshop Second Call for informal presentations and demonstrations The Coq workshop will take place on July 9th, as part as the FLoC federated conference in Edinburgh, Scotland. http://coq.inria.fr/coq-workshop/2010/cfp The Coq workshop will bring together Coq users, developers and contributors. The workshop will be organized from submitted, informal presentations, invited talks and a plenary discussion on the evolution and design of Coq. Topics of presentations may include any of the following ones: * Experiments with type-theoretic proof assistants * Language or tactics features * Theory and implementation of the Calculus of Inductive Constructions * Applications and experience in education and industry * Tools, platforms built on Coq * Plugins, libraries for Coq * Interfacing with Coq * Formalization tricks and Coq pearls Topics that have been experimented with in any flavor of type theory-based theorem proving and are relevant to the evolution of Coq may also be discussed during these informal presentations. Speakers wishing to present a demonstration should bring their own laptop computer or contact the program chair to arrange for a computer to host the demonstration. Descriptions of the proposed informal presentations should consist of abstracts of approximately 1000 words and be uploaded to the easychair system http://www.easychair.org/conferences/?conf=coq2 before May 10th. For further questions, please contact Yves Bertot. yves.ber...@sophia.inria.fr
[TYPES/announce] Coq-Workshop: Call for informal presentations (updated information)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Coq Workshop Second Call for informal presentations and demonstrations The Coq workshop will take place on July 9th, as part as the FLoC federated conference in Edinburgh, Scotland. http://coq.inria.fr/coq-workshop/2010/cfp The Coq workshop will bring together Coq users, developers and contributors. The workshop will be organized from submitted, informal presentations, invited talks and a plenary discussion on the evolution and design of Coq. Topics of presentations may include any of the following ones: * Experiments with type-theoretic proof assistants * Language or tactics features * Theory and implementation of the Calculus of Inductive Constructions * Applications and experience in education and industry * Tools, platforms built on Coq * Plugins, libraries for Coq * Interfacing with Coq * Formalization tricks and Coq pearls Topics that have been experimented with in any flavor of type theory-based theorem proving and are relevant to the evolution of Coq may also be discussed during these informal presentations. Speakers wishing to present a demonstration should bring their own laptop computer or contact the program chair to arrange for a computer to host the demonstration. Descriptions of the proposed informal presentations should consist of abstracts of approximately 1000 words and be uploaded to the easychair system http://www.easychair.org/conferences/?conf=coq2 before May 10th. For further questions, please contact Yves Bertot. yves.ber...@sophia.inria.fr
[TYPES/announce] Coq-workshop: Call for informal presentations
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Coq Workshop Call for informal presentations and demonstrations The Coq workshop will bring together Coq users, developers and contributors. The workshop will be organized from submitted, informal presentations, invited talks and a plenary discussion on the evolution and design of Coq. Topics of presentations may include any of the following ones: * Experiments with type-theoretic proof assistants * Language or tactics features * Theory and implementation of the Calculus of Inductive Constructions * Applications and experience in education and industry * Tools, platforms built on Coq * Plugins, libraries for Coq * Interfacing with Coq * Formalization tricks and Coq pearls Topics that have been experimented with in any flavor of type theory-based theorem proving and are relevant to the evolution of Coq may also be discussed during these informal presentations. Speakers wishing to present a demonstration should bring their own laptop computer or contact the program chair to arrange for a computer to host the demonstration. Descriptions of the proposed informal presentations should be uploaded to the easychair system http://www.easychair.org/conferences/?conf=coq-2 before May 10th. For further questions, please contact Yves Bertot. yves.ber...@sophia.inria.fr
[TYPES/announce] CFP: Call for papers, Coq Workshop (deadline March 22nd)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] lease help disseminate this call for papers Two changes in the call for papers: 1/ papers describing experiments in other type theory-based proof assistants are explicitly invited to this workshop, 2/ EPTCS (http://eptcs.org/) has agreed to host the proceedings. Call for papers The Coq workshop will bring together Coq users, developers and contributors. The workshop will be organized from submitted papers, invited talks and a plenary discussion on the evolution and design of Coq. Topics for submitting a paper include: * Experiments with type-theoretic proof assistants * Language or tactics features * Theory and implementation of the Calculus of Inductive Constructions * Applications and experience in education and industry * Tools, platforms built on Coq * Plugins, libraries for Coq * Interfacing with Coq * Formalization tricks and Coq pearls Authors should submit their paper through EasyChair at the following link: http://www.easychair.org/conferences/?conf=coq2 Submitted papers should be in (postscript or) portable document format. Papers should not exceed 12 pages in length in single-column full-page 11pt A4 style. If there is sufficient demand, we will try to organize a time slot for demonstrations. Similarly, we may also organize a session on the lessons learned from teaching Coq. If you are interested, please send a brief proposal. Venue FLoC 2010, Edinburgh, Scotland Important Dates * March 22nd: Deadline for submission of papers * May 1st: Acceptance Notification * May 31st: Final version of articles * July 9th: Workshop in Edinburgh Program Committee * Andrew Appel * Yves Bertot (Chair) * Adam Chlipala * Georges Gonthier * Benjamin Grégoire * Hugo Herbelin * Micaela Mayero * Christine Paulin-Mohring * Bas Spitters Contact yves.ber...@sophia.inria.fr
[TYPES/announce] CFP: Call for papers, Coq Workshop (Edinburgh, July 9)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] lease help disseminate this call for papers Two changes in the call for papers: 1/ papers describing experiments in other type theory-based proof assistants are explicitly invited to this workshop, 2/ EPTCS (http://eptcs.org/) has agreed to host the proceedings. Call for papers The Coq workshop will bring together Coq users, developers and contributors. The workshop will be organized from submitted papers, invited talks and a plenary discussion on the evolution and design of Coq. Topics for submitting a paper include: * Experiments with type-theoretic proof assistants * Language or tactics features * Theory and implementation of the Calculus of Inductive Constructions * Applications and experience in education and industry * Tools, platforms built on Coq * Plugins, libraries for Coq * Interfacing with Coq * Formalization tricks and Coq pearls Authors should submit their paper through EasyChair at the following link: http://www.easychair.org/conferences/?conf=coq2 Submitted papers should be in (postscript or) portable document format. Papers should not exceed 12 pages in length in single-column full-page 11pt A4 style. If there is sufficient demand, we will try to organize a time slot for demonstrations. Similarly, we may also organize a session on the lessons learned from teaching Coq. If you are interested, please send a brief proposal. Venue FLoC 2010, Edinburgh, Scotland Important Dates * March 22nd: Deadline for submission of papers * May 1st: Acceptance Notification * May 31st: Final version of articles * July 9th: Workshop in Edinburgh Program Committee * Andrew Appel * Yves Bertot (Chair) * Adam Chlipala * Georges Gonthier * Benjamin Grégoire * Hugo Herbelin * Micaela Mayero * Christine Paulin-Mohring * Bas Spitters
