http://blog.gmane.org/gmane.science.mathematics.prooftheory hourly 1 1901-01-01T00:00+00:00 http://gmane.org/img/gmane-25t.png http://gmane.org http://comments.gmane.org/gmane.science.mathematics.prooftheory/965 <pre>Call for Participation Explicit Paradigms in Logic and Computer Science June 4-6 2012 Bern, Switzerland http://www.expa12.unibe.ch/index.php For a preliminary PROGRAM scroll down to the end of this email Explicitness plays an important role in many parts of mathematics and computer science. Constructive and intuitionistic proofs, for example, provide explicit witnesses for existential assertions. In the area of explicit mathematics, operations and types are explicitly given by terms of the language. These traditional and well-established areas are complemented by more recent developments. Justification logics, the first of which was conceived 20 years ago in Bern, are natural extensions of modal logics with the capability of unfolding belief and knowledge modalities into explicit justification terms. Even more recent are infon logics, which have been developed in the context of distributed authorization and deal with pieces of information explicitly. The purpose of this workshop is to provide a platform for presenting new results in these research areas. INVITED SPEAKERS: Sergei Artemov (New York, NY) Lev Beklemishev (Moscow) Andreas Blass (Ann Arbor, MI) Samuel Bucheli (Bern) Wilfried Buchholz (Munich) — TBC Laura Crosilla (Leeds) Walter Dean (Coventry) Sebastian Eberhard (Bern) Melvin Fitting (New York, NY) Yuri Gurevich (Redmond, WA) Reinhard Kahle (Lisbon) Pierluigi Minari (Florence) Isabel Oitavem (Lisbon) Wolfram Pohlers (Münster) Michael Rathjen (Leeds) Anton Setzer (Swansea) Valentin Shehtman (Moscow) Tatiana Yavorskaya (Moscow) PROGRAM COMMITTEE: Gerhard Jäger (Chair) Roman Kuznets Thomas Strahm Thomas Studer PRELIMINARY PROGRAM: Monday, June 4 9:15 – 10:00Valentin Shehtman TBA 10:00 – 10:30Coffee break 10:30 – 11:15Laura Crosilla "Operations and sets, constructively" 11:30 – 12:00Sebastian Eberhard "Applicative theories for logarithmic complexity classes" Lunch break 14:00 – 14:45Sergei Artemov "A classical view of constructive semantics" 14:45 – 15:15Coffee break 15:15 – 16:00Pierluigi Minari "Labelled sequent calculi for modal logics: getting rid of hidden contractions" 16:15 – 17:00Wolfram Pohlers "Some applications of semiformal systems" Tuesday, June 5 9:15 – 10:00Michael Rathjen "The existence property and ordinal analysis" 10:00 – 10:30Coffee break 10:30 – 11:15Lev Beklemishev "Topological semantics of provability logic" 11:30 – 12:00Samuel Bucheli "A justification logic with common knowledge" Lunch break 14:00 – 14:45Yuri Gurevich "What, if anything, can be done in linear time?" 14:45 – 15:15Coffee break 15:15 – 16:00Andreas Blass "Logical justification in distributed authorization" 16:15 – 17:00Anton Setzer "Inductive-inductive definitions" Social dinner Wednesday, June 6 9:15 – 10:00Tatiana Yavorskaya "Arithmetical semantics for the first order logic of proofs" 10:00 – 10:30Coffee break 10:30 – 11:15Isabel Oitavem "The class NP" 11:30 – 12:00Walter Dean "Gödel, Kreisel, and the origin of the Logic of Proofs" Lunch break 14:00 – 14:45Reinhard Kahle "Induction schemata for classes of computational complexity" 14:45 – 15:15Coffee break 15:15 – 16:00Melvin Fitting "Possible world semantics for first order LP" </pre> Thomas Studer 2012-05-22T12:46:36 http://comments.gmane.org/gmane.science.mathematics.prooftheory/964 <pre>Greetings to all! This is the second announcement for the fifth workshop "Réalisabilité à Chambéry". This year's workshop will take place from Tuesday the 5th of June to Friday the 8th of June. The invited speakers are: - Martin Hofmann (Munich): "Proof-relevant logical relations", - Jonas Frey (Paris): "Basic relational objects as an algebraic framework for realizability" - Jean-Louis Krivine (Paris): classical realizability, TBA, - Alexandre Miquel (Lyon): realizability model for set theory, TBA. The program will be made available shortly here: http://lama.univ-savoie.fr/~hyvernat/Realisabilite2012/program.php Note that the meeting will start on Tuesday the 5th, at 2'00 pm. Partial information is gathered on the web page: http://lama.univ-savoie.fr/~hyvernat/Realisabilite2012/ and you can (should) register for the workshop there: http://lama.univ-savoie.fr/~hyvernat/Realisabilite2012/registration.php There will be sessions for contributed talks, and PhD students are particularly encouraged to submit a talk. (There are very few submissions at this time: don't hesitate to submit something...) For the first time, we will offer a couple of grants for students attending the workshop. Those grants will cover (part of) the cost of the travel and a room on the campus. We still don't know how many grants we will be able to award, but priority will be given to students presenting their work at the workshop. If you are interested, register and contact me as soon as possible... It is possible to get a student room (on campus, very cheap, but only a bare room). Students will of course be given priority for those, but anyone may ask... You do have to register before the 25th of May though. Other possibilities for accommodation are given on the web page: http://lama.univ-savoie.fr/~hyvernat/Realisabilite2012/logistic.php </pre> Tom Hirschowitz 2012-05-20T18:58:59 http://comments.gmane.org/gmane.science.mathematics.prooftheory/963 <pre>[My department is advertising for a senior position in logic or philosophy of science. We are looking for a high-profile researcher at or near the Full Professor level who can build up the department's profile, attract and train graduate students in philosophy, and has experience obtaining outside funding. The job is pretty cushy, with a 1-1 teaching load, competitive pay, and is a tenured permanent position. Note that since this is a search under the CRC program there is no requirement to give preference to Canadians. The department's website is at http://www.phil.ucalgary.ca/] The Department of Philosophy at the University of Calgary invites applications and nominations for a Tier I Canada Research Chair in Logic and the Philosophy of Science. The Canada Research Chairs program has been established by the Government of Canada to enable Canadian universities to foster excellence in research and teaching. Further information on the program is available on the CRC website at www.chairs.gc.ca. We are seeking an established scholar and a leader in any area of logic or the philosophy of science. The successful candidate will have an outstanding record of research, teaching and graduate supervision, and an innovative research program. The appointment, at the rank of Associate Professor or Professor, is expected to start on July 1, 2013. Specific inquiries about this position may be directed to: Ali Kazmi, Head Department of Philosophy University of Calgary Email: akazmi-b/Twen6L8IQsA/PxXw9srA&lt; at &gt;public.gmane.org All Chairs are subject to review and final approval by the CRC Secretariat. Applications including a CV, a writing sample, a teaching dossier, and a description of a 7 year research plan, and names and contact information of three referees may be sent to: Merlette Schnell, Manager Department of Philosophy University of Calgary 2500 University Drive NW Calgary, Alberta T2N 1N4 CANADA Email: schnell-b/Twen6L8IQsA/PxXw9srA&lt; at &gt;public.gmane.org Applications will be accepted until the position is filled. Review of the applications will begin on July 9, 2012. </pre> Richard Zach 2012-05-19T20:23:18 http://comments.gmane.org/gmane.science.mathematics.prooftheory/962 <pre>The deadline for submitting to CPP 2012 is June 8, 2012. The Second International Conference on Certified Programs and Proofs (CPP 2012) CALL FOR PAPERS Kyoto, Japan December 13-15 2012 http://cpp12.kuis.kyoto-u.ac.jp/ co-located with APLAS 2012 http://aplas12.kuis.kyoto-u.ac.jp/ CPP is a new international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. We invite submissions on topics that fit under this rubric. The first CPP conference was held in Kenting, Taiwan during December 7-9, 2011. As with the first meeting, the proceedings will be published in Springer-Verlag's Lecture Notes in Computer Science series. Suggested, but not exclusive, specific topics of interest for submissions include: certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors; program logics, type systems, and semantics for certified code; certified decision procedures, mathematical libraries, and mathematical theorems; proof assistants and proof theory; new languages and tools for certified programming; program analysis, program verification, and proof-carrying code; certified secure protocols and transactions; certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; certificates for program termination; logics for certifying concurrent and distributed programs; higher-order logics, logical systems, separation logics, and logics for security; teaching mathematics and computer science with proof assistants; and "Proof Pearls" (elegant, concise, and instructive examples). IMPORTANT DATES: Authors are required to submit a paper title and a short abstract before submitting the full paper. The submission should include when necessary a url where to find the formal development assessing the essential aspects of the work. All submissions will be electronic. All deadlines are at midnight (GMT). Abstract Deadline: Friday, June 8, 2012 Paper Submission Deadline: Friday, June 15, 2012 Author Notification: Monday, August 27, 2012 Camera Ready: Monday, September 17, 2012 Conference: December 13-15, 2012 PROGRAM CO-CHAIRS: Chris Hawblitzel (Microsoft Research Redmond) Dale Miller (INRIA Saclay and LIX, Ecole Polytechnique) GENERAL CHAIR: Jacques Garrigue (Nagoya University) PROGRAM COMMITTEE: Stefan Berghofer (secunet Security Networks AG) Wei-Ngan Chin (National University of Singapore) Adam Chlipala (MIT) Mike Dodds (University of Cambridge) Amy Felty (University of Ottawa) Xinyu Feng (University of Science and Technology of China) Herman Geuvers (Radboud University, Nijmegen) Robert Harper (Carnegie Mellon University) Chris Hawblitzel (Microsoft Research Redmond) Gerwin Klein (NICTA) Laura Kovacs (Vienna University of Technology) Dale Miller (INRIA Saclay and LIX, Ecole Polytechnique) Rupak Majumdar (UCLA, Max Planck Institute for Software Systems) Lawrence Paulson (University of Cambridge) Frank Piessens (KU Leuven) Randy Pollack (Harvard and Edinburgh University) Bow-Yaw Wang (Academia Sinica) Santiago Zanella Béguelin (IMDEA Software Institute) ORGANIZING COMMITTEE: Jacques Garrigue and Atsushi Igarashi Email: cpp2012oc-knClnm2CsUbQYvvA02pP0Hf5DAMn2ifp&lt; at &gt;public.gmane.org CPP STEERING COMMITTEE: Andrew Appel (Princeton University) Nikolaj Bjørner (Microsoft Research Redmond) Georges Gonthier (Microsoft Research Cambridge) John Harrison (Intel Corporation) Jean-Pierre Jouannaud (co-Chair) (INRIA and Tsinghua University) Gerwin Klein (NICTA) Tobias Nipkow (Technische Universität München) Zhong Shao (co-Chair) (Yale University) SUBMISSION INSTRUCTIONS: Papers should be submitted electronically online via the conference submission web page at URL: http://www.easychair.org/conferences/?conf=cpp2012 Acceptable formats are PostScript or PDF, viewable by Ghostview or Acrobat Reader. Submissions should not exceed 16 pages in LNCS format, including bibliography and figures. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant. The proceedings of the symposium will be published as a volume in Springer-Verlag's Lecture Notes in Computer Science series. Each submission must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference, all phrased for the non-specialist. Technical and formal developments directed to the specialist should follow. Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS, Vampire, etc. References and comparisons with related work should be included. Papers not conforming to the above requirements concerning format and length may be rejected without further consideration. The results must be unpublished and not submitted for publication elsewhere, including the proceedings of other published conferences or workshops. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. Original formal proofs of known results in mathematics or computer science are among the targets. One author of each accepted paper is expected to present it at the conference. </pre> Chris Hawblitzel 2012-05-16T23:46:49 http://comments.gmane.org/gmane.science.mathematics.prooftheory/961 <pre> CALL FOR TALK PROPOSALS HOPE 2012 The 1st ACM SIGPLAN Workshop on Higher-Order Programming with Effects September 9, 2012 Copenhagen, Denmark (the day before ICFP 2012) http://hope2012.mpi-sws.org HOPE is a *new workshop* that is intended to bring together researchers interested in the design, semantics, implementation, and verification of higher-order effectful programs. It will be *informal*, consisting of invited talks, contributed talks on work in progress, and open-ended discussion sessions. This 1st edition of HOPE is dedicated to John Reynolds, whose work is an inspiration to us all. --------------------- Goals of the Workshop --------------------- A recurring theme in many papers at ICFP, and in the research of many ICFP attendees, is the interaction of higher-order programming with various kinds of effects: storage effects, I/O, control effects, concurrency, etc. While effects are of critical importance in many applications, they also make it hard to build, maintain, and reason about one's code. Higher-order languages (both functional and object-oriented) provide a variety of abstraction mechanisms to help "tame" or "encapsulate" effects (e.g. monads, ADTs, ownership types, typestate, first-class events, transactions, Hoare Type Theory, session types, substructural and region-based type systems), and a number of different semantic models and verification technologies have been developed in order to codify and exploit the benefits of this encapsulation (e.g. bisimulations, step-indexed Kripke logical relations, higher-order separation logic, game semantics, various modal logics). But there remain many open problems, and the field is highly active. The goal of the HOPE workshop is to bring researchers from a variety of different backgrounds and perspectives together to exchange new and exciting ideas concerning the design, semantics, implementation, and verification of higher-order effectful programs. We want HOPE to be as informal and interactive as possible. The program will thus involve a combination of invited talks, contributed talks about work in progress, and open-ended discussion sessions. There will be no published proceedings, but participants will be invited to submit working documents, talk slides, etc. to be posted on this website. ----------------------- Call for Talk Proposals ----------------------- We solicit proposals for contributed talks. Proposals should be at most 2 pages, in either plain text or PDF format, and should specify how long a talk the speaker wishes to give. By default, contributed talks will be 30 minutes long, but proposals for shorter or longer talks will also be considered. Speakers may also submit supplementary material (e.g. a full paper, talk slides) if they desire, which PC members are free (but not expected) to read. We are interested in talks on all topics related to the interaction of higher-order programming and computational effects. Talks about work in progress are particularly encouraged. If you have any questions about the relevance of a particular topic, please contact the PC chairs at the address hope2012-41PbBDiSz5ubup2nOX2J7Q&lt; at &gt;public.gmane.org Deadline for talk proposals: June 8, 2012 (Friday) Notification of acceptance: July 1, 2012 (Sunday) Workshop: September 9, 2012 (Sunday) The submission website is now open: http://www.easychair.org/conferences/?conf=hope2012 --------------------- Workshop Organization --------------------- Program Co-Chairs: Amal Ahmed (Northeastern University) Derek Dreyer (MPI-SWS, Germany) Program Committee: Jim Laird (University of Bath) Rasmus Møgelberg (IT University of Copenhagen) Greg Morrisett (Harvard University) Aleks Nanevski (IMDEA Software Institute) David Naumann (Stevens Institute of Technology) Matthew Parkinson (Microsoft Research Cambridge) François Pottier (INRIA Rocquencourt) Amr Sabry (Indiana University) Eijiro Sumii (Tohoku University) Nikhil Swamy (Microsoft Research Redmond) Nobuko Yoshida (Imperial College London)</pre> Amal Ahmed 2012-05-16T19:04:20 http://comments.gmane.org/gmane.science.mathematics.prooftheory/960 <pre>JELIA 2012 CALL FOR PAPERS ========================== 12th European Conference on Logics in Artificial Intelligence - Toulouse, France, September 26-28, 2012 http://www.irit.fr/jelia2012 Logics provide a formal basis and key descriptive notation for the study and development of applications and systems in Artificial Intelligence (AI). With the depth and maturity of formalisms, methodologies, and systems today, such logics are increasingly important. The European Conference on Logics in Artificial Intelligence (or Journees Europeennes sur la Logique en Intelligence Artificielle --- JELIA) began back in 1988, as a workshop, in response to the need for a European forum for the discussion of emerging work in this field. Since then, JELIA has been organized biennially, with English as the official language, and with proceedings published in Springer-Verlag's Lecture Notes in Artificial Intelligence series. In 2012 the conference is organized in Toulouse, France. The increasing interest in this forum, its international level with growing participation from researchers outside Europe, and the overall technical quality, has turned JELIA into a major forum for the discussion of logic-based approaches to AI. Aims and Scope ============== The aim of JELIA 2012 is to bring together active researchers interested in all aspects concerning the use of logics in Artificial Intelligence to discuss current research, results, problems, and applications of both theoretical and practical nature. JELIA strives to foster links and facilitate cross-fertilization of ideas among researchers from various disciplines, among researchers from academia and industry, and between theoreticians and practitioners. Authors are invited to submit papers presenting original and unpublished research in all areas related to the use of logics in Artificial Intelligence including: </pre> Andreas Herzig 2012-05-16T12:47:04 http://comments.gmane.org/gmane.science.mathematics.prooftheory/959 <pre>E. W. Beth Dissertation Prize: 2012 new call for nominations Since 2002, FoLLI (the Association for Logic, Language, and Information, http://www.folli.org) awards the E.W. Beth Dissertation Prize to outstanding dissertations in the fields of Logic, Language, and Information. We invite submissions for the best dissertation which resulted in a Ph.D. degree in the year 2011. The dissertations will be judged on technical depth and strength, originality, and impact made in at least two of three fields of Logic, Language, and Computation. Interdisciplinarity is an important feature of the theses competing for the E.W. Beth Dissertation Prize. Who qualifies. Nominations of candidates are admitted who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2011 and December 31st, 2011. There is no restriction on the nationality of the candidate or the university where the Ph.D. was granted. After a careful consideration, FoLLI has decided to accept only dissertations written in English. Dissertations produced in 2011 but not written in English or not translated will be allowed for submission, after translation, also with the call next year (for dissertations defended in 2012). The present call for nominations for the E.W. Beth Disertation Award 2012 will also accept nominations of full English translations of theses originally written in another language than English and defended in 2010 or 2011. Prize. The prize consists of: -a certificate -a donation of 2500 euros provided by the E.W. Beth Foundation -an invitation to submit the thesis (or a revised version of it) to the FoLLI Publications on Logic, Language and Information (Springer). For further information on this series see the FoLLI site. How to submit. Only electronic submissions are accepted. The following documents are required: 1. The thesis in pdf or ps format (doc/rtf not accepted); 2. A ten page abstract of the dissertation in ascii or pdf format; 3. A letter of nomination from the thesis supervisor. Self-nominations are not admitted: each nomination must be sponsored by the thesis supervisor. The letter of nomination should concisely describe the scope and significance of the dissertation and state when the degree was officially awarded; 4. Two additional letters of support, including at least one letter from a referee not affiliated with the academic institution that awarded the Ph.D. degree. All documents must be submitted electronically to buszko-aUYh8w+s/F86AUDyBy5rKQ&lt; at &gt;public.gmane.org Hard copy submissions are not admitted. In case of any problems with the email submission or a lack of notification within three working days, nominators should write to buszko-aUYh8w+s/F86AUDyBy5rKQ&lt; at &gt;public.gmane.org Important dates: Deadline for Submissions: May 1, 2012. Extended: June 30, 2012. Notification of Decision: July 31, 2012. Explanation: Due to some technical obstacles, the first call for nominations was announced on the site of FoLLI in the beginning of March 2012 but not widely distributed through mailing lists. Therefore we essentially prolong the deadline now. We ask all potential nominators to inform the chair earlier by a mail to buszko-aUYh8w+s/F/VItvQsEIGlw&lt; at &gt;public.gmane.org, even before having completed the required documents. Committee : Chris Barker (New York) Wojciech Buszkowski (chair) (Poznan) Dale Miller (Palaiseau) Larry Moss (Bloomington) Ian Pratt-Hartmann (Manchester) Ruy de Queiroz (Recife) Giovanni Sambin (Padua) Rob van der Sandt (Nijmegen) Rineke Verbrugge (Groningen) Heinrich Wansing (Bochum) </pre> A. Herzig 2012-05-15T08:01:59 http://comments.gmane.org/gmane.science.mathematics.prooftheory/958 <pre>[We apologize if you have received multiple copies of this message] ***************************************************************** ------ GandALF 2012 ----- ***************************************************************** Third International Symposium on Games, Automata, Logics, and Formal Verification Napoli, Italy, September 6th-8th, 2012 http://www.gandalf.unina.it Co-located with GAMES 2012 ****************************************************** | CALL FOR PAPERS (EXTENDED DEADLINE) | ****************************************************** OBJECTIVES The aim of the symposium is to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. The idea is to cover an ample spectrum of themes, ranging from theory to applications, and stimulate cross-fertilization. Papers focused on formal methods are especially welcome. Authors are invited to submit original research or tool papers on all relevant topics in these areas. Papers discussing new ideas that are at an early stage of development are also welcome. LIST OF TOPICS The topics covered by the conference include, but are not limited to, the following: Automata Theory Automated Deduction Computational aspects of Game Theory Concurrency and Distributed computation Decision Procedures Deductive, Compositional, and Abstraction Techniques for Verification Finite Model Theory First-order and Higher-order Logics Formal Languages Formal Methods for Complex Systems (e.g., Interactive Systems, Systems Biology) Games and Automata for Verification Game Semantics Hybrid, Embedded, and Mobile Systems Verification Logical aspects of Computational Complexity Logics of Programs Modal and Temporal Logics Model Checking Models of Reactive and Real-Time Systems Program Analysis and Software Verification Run-time Verification and Testing Specification and Verification of Finite and Infinite-state Systems Synthesis CO-LOCATED EVENT GAMES 2012, Annual Workshop of the ESF Networking Programme on Games for Design and Verification (http://www.games.unina.it/). INVITED SPEAKERS Alberto Policriti (University of Udine, Italy). Moreover, we plan to have joint invited speakers with the co-located GAMES meeting. PAPER SUBMISSION Submitted papers should not exceed fourteen (14) pages using EPTCS format, be unpublished and contain original research. For papers reporting experimental results, authors are encouraged to make their data available with their submission. Submissions must be in PDF or PS format and will be handled via EasyChair. IMPORTANT DATES Abstract submission May 16, 2012 (EXTENDED) Paper submission May 22, 2012 (EXTENDED) Acceptance notification June 27, 2012 Final version July 15, 2012 Conference September 6-8, 2012 PROCEEDINGS The proceedings will be published by Electronic Proceedings in Theoretical Computer Science. A special issue of a major international journal to publish an extended and revised version of the best symposium papers is also under consideration. Revised versions of the selected papers from the previous editions lead to two special issues of the International Journal of Foundation of Computer Science and of Theoretical Computer Science, respectively. PROGRAM CHAIRS Marco Faella (Universita’ di Napoli "Federico II", Italy) Aniello Murano (Universita’ di Napoli "Federico II", Italy) PROGRAM COMMITTEE Veronique Bruyere (Universite' de Mons-Hainaut, Belgium) Agostino Cortesi (Universita' Ca' Foscari di Venezia, Italy) Luca de Alfaro, (University of California at Santa Cruz, USA) Kousha Etessami, (University of Edinburgh, UK) Erich Grädel, (RWTH Aachen University, Germany) Arie Gurfinkel, (Carnegie Mellon University, USA) Orna Kupferman, (Hebrew Unversity, Israel) Martin Lange, (University of Kassel, Germany) Carsten Lutz, (University of Bremen, Germany) Oded Maler (CNRS-VERIMAG, University of Grenoble, France) Nicolas Markey, (LSV, CNRS &amp; ENS Cachan, France) Anca Muscholl, (University of Bordeaux, France) Margherita Napoli, (Universita’ di Salerno , Italy) Damian Niwinski (University of Warsaw, Poland) Carla Piazza, (University of Udine, Italy) Nir Piterman, (University of Leicester,UK) Gabriele Puppis, (University of Oxford, UK) Ramaswamy Ramanujam, (IMSC Chennai, India) Sven Schewe, (University of Liverpool, UK) Natasha Sharygina, (University of Lugano, Switzerland) Marielle Stoelinga, (University of Twente, Netherlands) Enrico Tronci, (Universita’ di Roma "La Sapienza", Italy) Helmut Veith, (TU Vienna, Austria) Tiziano Villa, (Universita’ di Verona, Italy) Mahesh Viswanathan, (University of Illinois, USA) STEERING COMMITTEE Mikolaj Bojanczyk (University of Warsaw, POLAND) Javier Esparza (University of Munich, GERMANY) Angelo Montanari (University of Udine, ITALY) Margherita Napoli (University of Salerno, ITALY) Mimmo Parente (University of Salerno, ITALY) Wolfgang Thomas (RWTH Aachen University, GERMANY) Wieslaw Zielonka (University of Paris7, FRANCE) ADVISORY BOARD Stefano Crespi Reghizzi (University of Milan, ITALY) Jozef Gruska (Masaryk University, CZECH REPUBLIK) Oscar H. Ibarra (University of California, USA) Andrea Maggiolo-Schettini (University of Pisa, ITALY) INFO Please visit the conference website (http://www.gandalf.unina.it) for more information </pre> Nello Murano 2012-05-10T14:29:00 http://comments.gmane.org/gmane.science.mathematics.prooftheory/957 <pre>Hello, I would like to advertise the following positions at the University of Bath. In particular we are looking for applicants in the area `Software verification and correctness´. Ciao, -Alessio Software verification and correctness We aim to build on the existing strengths within the Mathematical Foundations group in the Department of Computer Science. The group comprises Prof Guy McCusker and Dr Jim Laird (semantics), Dr Alessio Guglielmi (proof theory), Dr John Power (category theory) and Prof James Davenport (computer algebra). We seek to strengthen its activities via the appointment of a Prize Fellow in software verification &amp; correctness, to be understood broadly, to complement existing expertise; it would also be desirable to strengthen connections with other groups in the department, particularly with Dr Marina De Vos and Dr Julian Padget in the Intelligent Systems group. The Fellow would be coming into a well-resourced, lively group that runs a weekly seminar series, which once a month is jointly held with Swansea's Proofs, Complexity and Verification seminar. The Math Foundations group belongs to the Wessex Theory Seminar, comprising the Computer Science Departments of Bath, Oxford, Southampton, Cambridge, Imperial College, Queen Mary, Sussex and Swansea. The group has a good track record of nurturing early career researchers. For informal inquiries contact Prof Guy McCusker: G.A.McCusker AT bath.ac.uk ------------------------------------------------------------------------------------- Prize Fellow - Department of Computer Science Salary: Starting from £37,012, rising to £44,166 Closing Date: Monday 21 May 2012 Interview Date: See advert Reference: JK1000 To further enhance our academic base, we are making a strategic investment in recruiting University of Bath Prize Fellows across all disciplines. This is an opportunity for outstanding post-doctoral researchers to develop their academic career in a supportive and well-resourced research environment. In the Faculty of Science we will appoint a total of six Fellows to further strengthen and develop areas of existing research excellence. In the Department of Computer Science we invite applications in the areas of: * Machine Learning * Software Verification and Correctness * Modelling Behaviour Transmission Details of these priority areas and the Faculty-wide appointment process can be found here: &lt;http://www.bath.ac.uk/science/prize-fellows&gt;. The Fellows will be expected to pursue an independent programme of research, including publishing in top quality journals and securing external research grants. The initial appointment will be to a fixed-term Research Fellow post with the expectation of transfer to a permanent lectureship at the end of year two, or exceptionally at the end of year three. Applicants should upload a CV and a 2-page outline of their research plans over the next 3-5 years, showing how these complement and enhance existing research within the relevant priority area. Interviews will take place on Friday 29th June or Monday 2nd July 2012. </pre> Alessio Guglielmi 2012-05-10T09:11:45 http://comments.gmane.org/gmane.science.mathematics.prooftheory/956 <pre>******************************************************************************** CALL FOR PARTICIPATION AT ESSLLI 2012 Meeting: 24th European Summer School in Logic, Language and Information (ESSLLI) Date: 06-Aug-2012 - 17-Aug-2012 Location: Opole, Poland Meeting URL: http://www.esslli2012.pl Early registration deadline: 15-06-2012 ******************************************************************************** **Meeting Description** For the past 24 years, the European Summer School in Logic, Language and Information (ESSLLI) has been organized every year by the Association for Logic, Language and Information (FoLLI) in different sites around Europe. The main focus of ESSLLI is on the interface between linguistics, logic and computation. ESSLLI offers foundational, introductory and advanced courses, as well as workshops, covering a wide variety of topics within the three areas of interest: Language and Computation, Language and Logic, and Logic and Computation. Previous summer schools have been highly successful, attracting up to 500 students from Europe and elsewhere. The school has developed into an important meeting place and forum for discussion for students and researchers interested in the interdisciplinary study of Logic, Language and Information. During two weeks, 49 courses and 6 workshops are offered to the attendants, each of 1.5 hours per day during a five days week, with up to seven parallel sessions. ESSLLI also includes a student session (papers and posters by students only, 1.5 hour per day during the two weeks). There will be three evening lectures by Mel Fitting, Jonathan Ginzburg and Adam Przepiorkowski. In 2012, ESSLLI will held in Opole, Poland and will be organized by the University of Opole, Poland. Chair of the program committee is Andreas Herzig, and chairs of the organizing committee are Urszula Wybraniec-Skardowska and Janusz Czelakowski. **Summer School Programme** http://www.esslli2012.pl/index.php?id=67 **Online Registration** http://www.esslli2012.pl/index.php?id=68 **Programme Committee** Chair: Andreas Herzig (Université de Toulouse and CNRS) Local co-chair: Anna Pietryga (University of Opole) Area specialists: Language and Computation: - Miriam Butt (Sprachwissenschaft, University of Konstanz) - Gosse Bouma (Groningen University) Language and Logic: - Regine Eckardt (Language and Literature, University of Göttingen) - Rick Nouwen (UiL-OTS, Utrecht University) Logic and Computation: - Natasha Alechina (CS, University of Nottingham) - Andreas Weiermann (Mathematics and Computation, Ghent University) **Organizing Committee** Chair: Urszula Wybraniec-Skardowska and Janusz Czelakowski (University of Opole) </pre> A. Herzig 2012-05-09T15:30:00 http://comments.gmane.org/gmane.science.mathematics.prooftheory/955 <pre> ------------------------------------------------------------------ Call for Course and Workshop Proposals ESSLLI 2013 25th European Summer School in Logic, Language and Information Duesseldorf, Germany August 5-16, 2013 http://esslli2013.de/ ------------------------------------------------------------------ IMPORTANT DATES =============== 15 June 2012: Proposal submission deadline 15 September 2012: Notification 1 June 2013: Course material due TOPICS AND FORMAT ================= Proposals for courses and workshops at ESSLLI'2013 are invited in all areas of Logic, Linguistics and Computing and Information Sciences. Cross-disciplinary and innovative topics are particularly encouraged. Each course and workshop will consist of five 90 minute sessions, offered daily (Monday-Friday) in a single week. Proposals for two-week courses should be structured and submitted as two independent one-week courses, e.g. as an introductory course followed by an advanced one. In such cases the ESSLLI programme committee reserves the right to accept just one of the two proposals. All instructional and organizational work at ESSLLI is performed completely on a voluntary basis, so as to keep participation fees to a minimum. However, organizers and instructors have their registration fees waved, and are reimbursed for travel and accommodation expenses up to a level to be determined and communicated with the proposal notification. ESSLLI can only guarantee reimbursement for at most one course/workshop organizer, and can not guarantee full reimbursement of travel costs for lecturers or organizers from outside of Europe. The ESSLLI organizers would appreciate any help in controlling the School's expenses by seeking complete coverage of travel and accommodation expenses from other sources. CATEGORIES ========== Each proposal should fall under one of the following categories. * FUNDAMENTAL COURSES * Such courses are designed to present the basics of a research area, to people with no prior knowledge in that area. They should be of elementary level, without prerequisites in the course's topic, though possibly assuming a level of general scientific maturity in the relevant discipline. They should enable researchers from related disciplines to develop a level of comfort with the fundamental concepts and techniques of the course's topic, thereby contributing to the interdisciplinary nature of our research community. * INTRODUCTORY COURSES * Introductory courses are central to ESSLLI's mission. They are intended to introduce a research field to students, young researchers, and other non-specialists, and to foster a sound understanding of its basic methods and techniques. Such courses should enable researchers from related disciplines to develop some comfort and competence in the topic considered. Introductory courses in a cross-disciplinary area may presuppose general knowledge of the related disciplines. * ADVANCED COURSES * Advanced courses are targeted primarily to graduate students who wish to acquire a level of comfort and understanding in the current research of a field. * WORKSHOPS * Workshops focus on specialised, usually topics of current interest. Workshops organisers are responsible for solliciting papers and selecting the workshop programme. PROPOSAL GUIDELINES =================== Course and workshop proposals should follow closely the following guidelines to ensure full consideration. Each course may have no more than two instructors, and each workshop no more than two organizers. All instructors and organizers must possess a PhD or equivalent degree by the submission deadline. Course proposals should mention explicitly the intended course category. Proposals for introductory courses should indicate the intended level, for example as it relates to standard textbooks and monographs in the area. Proposals for advanced courses should specify the prerequisites in detail. Proposals must be submitted in PDF format via: https://www.easychair.org/conferences/?conf=esslli2013 and include all of the following: o Personal information for each proposer: Name, affiliation, contact address, email, fax, homepage (optional) o General proposal information: Title, category o Contents information * Abstract of up to 150 words * Motivation and description (up to two pages) * Tentative outline * Expected level and pre-requisites * Appropriate references (e.g. textbooks, monographs, proceedings, surveys) o Practical information: * Relevant preceding meetings and events, if applicable * Potential external funding for participants ------------------------------------------------------------------ </pre> Johan Bos 2012-05-09T09:48:06 http://comments.gmane.org/gmane.science.mathematics.prooftheory/954 <pre>------------------------------------------------------------------------------ Call For Papers Workshop on Logics for Resources, Processes and Programs (LRPP 2012) 1st July 2012, Manchester, UK (affiliated with IJCAR 2012, Manchester, UK) http://www.loria.fr/~galmiche/LRPP2012.html Extended deadline: May 20, 2012 ---------------------------------------------------------------------- A one day workshop on `Logics for Resources, Processes, and Programs' will be held the 1st July 2012 in conjunction with the IJCAR 2012 Conference in Manchester, UK, with D. Galmiche and D. Pym as organizers. The purpose of this workshop would be to discuss recent results on logics, including systems formulated in the style of Hoare and Hennessy-Milner, for modelling resources, processes, programs, and their interactions. We envisage a range of perspectives: proof-theoretic foundations, including decidability and complexity; semantic foundations (e.g., new resource semantics); specification of properties and behaviours; verification and analysis of programs and systems. It should help to establish and publicize a research agenda for such logics and their use in the development of trusted systems. The workshop is intended to provide a forum for discussion between researchers interested in logics of resources (from foundations to related calculi and applications) and researchers interested in languages and methods for specification of mobile, distributed, concurrent systems and their verification. Topics of interest include, but are not restricted to, the following: - Logics for resources: semantics and proof theory; - Process calculi, concurrency, resource-distribution; - Reasoning about programs and systems; - Extensions of logics; e.g., with modalities; - Languages of assertions, languages based on resource logics (query languages, pointers, trees, and graphs) and reasoning; - Theorem proving and model checking in resource logics: decision procedures, strategies, complexity results. KEYNOTE SPEAKER Peter O'Hearn (UCL, London,UK) SUBMISSIONS Researchers interested in presenting their works are invited to send an extended abstract (up to 10 pages) by e-mail submissions of PDF files to D. Galmiche (Didier.Galmiche-/zGXu1G9BXs&lt; at &gt;public.gmane.org) and D. Pym (d.j.pym-9qr1vRpWqPK1Qrn1Bg8BZw&lt; at &gt;public.gmane.org) by May 20th 2012. Papers will be reviewed by peers, typically members of the Programme Committee. Additional information will be available through WWW address: http://www.loria.fr/~galmiche/LRPP2012.html. Hardcopies of the preliminary proceedings will be distributed at the workshop and a Special Issue of a Journal on these topics is expected after the workshop. PROGRAM COMMITTEE J. Brotherston (Queen Mary, London, UK) M. Collinson (University of Aberdeen, Scotland) D. Galmiche (LORIA, Nancy, France: Co-chair) J. Harland (RMIT University, Melbourne, Australia) M. Hennessy (Trinity College, Dublin, Ireland) D. Larchey-Wendling (LORIA, Nancy, France) F. Pfenning (CMU, Pittsburgh, USA) D. Pym (University of Aberdeen, Scotland: Co-chair) IMPORTANT DATES Submissions: May 20, 2012 Notifications: May 30, 2012 Final papers: June 10, 2004 Workshop date: July 1st, 2012 MORE INFORMATION E-mail: Didier.Galmiche-/zGXu1G9BXs&lt; at &gt;public.gmane.org and d.j.pym-9qr1vRpWqPK1Qrn1Bg8BZw&lt; at &gt;public.gmane.org The University of Aberdeen is a charity registered in Scotland, No SC013683. </pre> Pym, Professor David J. 2012-05-08T17:30:47 http://comments.gmane.org/gmane.science.mathematics.prooftheory/953 <pre>8th SCANDINAVIAN LOGIC SYMPOSIUM 20-21 August 2012 at Roskilde University, DENMARK Third Announcement and Call for Papers The 8th Scandinavian Logic Symposium will be held at Roskilde University, Trekroner, Denmark, 20-21 August 2012. After a gap of fifteen years, the Scandinavian Logic Symposium is back. The Symposium is the first major initiative of the newly revived Scandinavian Logic Society (SLS, http://scandinavianlogic.org/) and will be held at Roskilde University (RUC), Denmark. As with previous editions of this conference, the aim of the programme is to reflect current activity in logic in our part of the world. So we hope that participants from Scandinavia, the Baltic countries and Northwestern Russia will take the opportunity to contribute a talk and to meet with fellow logicians from the area. But needless to say, we also extend a warm welcome to logicians from further afield and plan to present a varied and interesting collection of invited and contributed talks. TOPICS The scope of SLS 2012 is broad, ranging over the whole area of mathematical and philosophical logic, and logical methods in computer science. Suitable topics include (but are not limited to): * Proof Theory and Constructivism * Model Theory (including Finite Model Theory) * Set Theory * Computability Theory * Categorical Logic * Logic and Provability * Logic and Computer Science * Logic and Linguistics * Modal, Hybrid, Temporal, and Description Logic * Logics of Games, Dynamics and Interaction * Philosophy of Mathematics * Philosophy of Computation * Philosophy of Logic * Philosophical Logic PREVIOUS SCANDINAVIAN LOGIC SYMPOSIA: 7th Scandinavian Logic Symposium: Uppsala in 1996 6th Scandinavian Logic Symposium: Telemark in 1982 5th Scandinavian Logic Symposium: Aalborg in 1979 4th Scandinavian Logic Symposium: Jyväskylä in 1976 3rd Scandinavian Logic Symposium: Uppsala in 1973 2nd Scandinavian Logic Symposium: Oslo in 1971 1st Scandinavian Logic Symposium: Åbo in 1968 The proceedings of several of these meetings have been published in book form. INVITED SPEAKERS The Program Committee is delighted to announce the names of the four invited speakers: * Nikolaj Bjorner&lt;http://research.microsoft.com/en-us/people/nbjorner/&gt; * Rosalie Iemhoff&lt;http://www.phil.uu.nl/%7Eiemhoff/&gt; (sponsored by The Danish Network for the History and Philosophy of Mathematics) * Per Martin-Löf&lt;http://en.wikipedia.org/wiki/Per_Martin-L%C3%B6f&gt; * Boban Velickovic&lt;http://www.logique.jussieu.fr/%7Eboban/&gt; &lt;http://research.microsoft.com/en-us/people/nbjorner/&gt; SLS TUTORIALS On August 22nd, the day after the symposium finishes, a number of tutorials for PhD-students (or anyone else who is interested) will be given. These are intended to start from a relatively elementary level and lead on to current research problems. The following tutorial lectures have been confirmed so far: * Lars Kristiansen&lt;http://folk.uio.no/larsk/&gt; - "Honest subrecursive degree theory" * Sara Negri &lt;http://www.helsinki.fi/%7Enegri/&gt; - "Labelled proof systems for modal logic" * M. H. Sørensen&lt;http://www.formalit.dk/&gt; - "Curry-Howard Isomorphism" RELATED EVENTS: Also note that Advances in Modal Logic (AiML) will be held on 22-25 August 2012, Copenhagen, Denmark. URL:http://hylocore.ruc.dk/aiml2012/ PROGRAM COMMITTEE Co-chairs: Neil Jones (Copenhagen) and Erik Palmgren (Stockholm) Members: Torben Brauner (Roskilde) Peter Dybjer (Chalmers) Lars Kristiansen (Oslo) Øystein Linnebo (Birkbeck) Sara Negri (Helsinki) Dag Normann (Oslo) Asger Törnquist, (Vienna) Jouko Väänänen (Helsinki) ORGANISING COMMITTEE Patrick Blackburn (RUC), Klaus Frovin Jørgensen (RUC), Stig Andur Petersen (RUC) SUBMISSIONS Abstracts of talks should be submitted by May 1, 2012** using the EasyChair system https://www.easychair.org/conferences/?conf=sls2012 The abstracts may not exceed 3 pages (including bibliography) and should be in PDF format. **UPDATE: SUBMISSION DATE has been extended: 1 June NOTIFICATION OF ACCEPTANCE: 15 June STUDENT GRANTS We are happy to announce that the ASL is sponsoring SLS2012. Among other things, this means that student ASL members may apply for ASL travel funds that are available for sponsored meetings. (see http://www.aslonline.org/studenttravelawards.html). LOCATION Roskilde University (RUC) is situated at Trekroner, a small town 20 minutes by train from Central Copenhagen, and five minutes by train from Roskilde. ACCOMMODATION Most people who work at RUC and almost all the RUC students live in Copenhagen. Getting to RUC is an easy train journey from the centre of Copenhagen. We anticipate that most conference attendees will book hotels in central Copenhagen, where there are many hotels in many price ranges. Hotel accommodation can also be found in Roskilde, though there the options are more limited. REGISTRATION The conference website will be found at: http://scandinavianlogic.weebly.com/ Details concerning registration will be posted there in due course. </pre> Thomas Bolander 2012-05-01T13:31:30 http://comments.gmane.org/gmane.science.mathematics.prooftheory/952 <pre> 8th SCANDINAVIAN LOGIC SYMPOSIUM 20-21 August 2012 at Roskilde University, DENMARK Third Announcement and Call for Papers The 8th Scandinavian Logic Symposium will be held at Roskilde University, Trekroner, Denmark, 20-21 August 2012. After a gap of fifteen years, the Scandinavian Logic Symposium is back. The Symposium is the first major initiative of the newly revived Scandinavian Logic Society (SLS, http://scandinavianlogic.org/) and will be held at Roskilde University (RUC), Denmark. As with previous editions of this conference, the aim of the programme is to reflect current activity in logic in our part of the world. So we hope that participants from Scandinavia, the Baltic countries and Northwestern Russia will take the opportunity to contribute a talk and to meet with fellow logicians from the area. But needless to say, we also extend a warm welcome to logicians from further afield and plan to present a varied and interesting collection of invited and contributed talks. TOPICS The scope of SLS 2012 is broad, ranging over the whole area of mathematical and philosophical logic, and logical methods in computer science. Suitable topics include (but are not limited to): Proof Theory and Constructivism Model Theory (including Finite Model Theory) Set Theory Computability Theory Categorical Logic Logic and Provability Logic and Computer Science Logic and Linguistics Modal, Hybrid, Temporal, and Description Logic Logics of Games, Dynamics and Interaction Philosophy of Mathematics Philosophy of Computation Philosophy of Logic Philosophical Logic PREVIOUS SCANDINAVIAN LOGIC SYMPOSIA: 7th Scandinavian Logic Symposium: Uppsala in 1996 6th Scandinavian Logic Symposium: Telemark in 1982 5th Scandinavian Logic Symposium: Aalborg in 1979 4th Scandinavian Logic Symposium: Jyväskylä in 1976 3rd Scandinavian Logic Symposium: Uppsala in 1973 2nd Scandinavian Logic Symposium: Oslo in 1971 1st Scandinavian Logic Symposium: Åbo in 1968 The proceedings of several of these meetings have been published in book form. INVITED SPEAKERS The Program Committee is delighted to announce the names of the four invited speakers: Nikolaj Bjorner Rosalie Iemhoff (sponsored by The Danish Network for the History and Philosophy of Mathematics) Per Martin-Löf Boban Velickovic SLS TUTORIALS On August 22nd, the day after the symposium finishes, a number of tutorials for PhD-students (or anyone else who is interested) will be given. These are intended to start from a relatively elementary level and lead on to current research problems. The following tutorial lectures have been confirmed so far: Lars Kristiansen - "Honest subrecursive degree theory" Sara Negri - "Labelled proof systems for modal logic" M. H. Sørensen - "Curry-Howard Isomorphism" RELATED EVENTS: Also note that Advances in Modal Logic (AiML) will be held on 22-25 August 2012, Copenhagen, Denmark. URL: http://hylocore.ruc.dk/aiml2012/ PROGRAM COMMITTEE Co-chairs: Neil Jones (Copenhagen) and Erik Palmgren (Stockholm) Members: Torben Brauner (Roskilde) Peter Dybjer (Chalmers) Lars Kristiansen (Oslo) Øystein Linnebo (Birkbeck) Sara Negri (Helsinki) Dag Normann (Oslo) Asger Törnquist, (Vienna) Jouko Väänänen (Helsinki) ORGANISING COMMITTEE Patrick Blackburn (RUC), Klaus Frovin Jørgensen (RUC), Stig Andur Petersen (RUC) SUBMISSIONS Abstracts of talks should be submitted by May 1, 2012** using the EasyChair system https://www.easychair.org/conferences/?conf=sls2012 The abstracts may not exceed 3 pages (including bibliography) and should be in PDF format. **UPDATE: SUBMISSION DATE has been extended: 1 June NOTIFICATION OF ACCEPTANCE: 15 June STUDENT GRANTS We are happy to announce that the ASL is sponsoring SLS2012. Among other things, this means that student ASL members may apply for ASL travel funds that are available for sponsored meetings. (see http://www.aslonline.org/studenttravelawards.html). LOCATION Roskilde University (RUC) is situated at Trekroner, a small town 20 minutes by train from Central Copenhagen, and five minutes by train from Roskilde. ACCOMMODATION Most people who work at RUC and almost all the RUC students live in Copenhagen. Getting to RUC is an easy train journey from the centre of Copenhagen. We anticipate that most conference attendees will book hotels in central Copenhagen, where there are many hotels in many price ranges. Hotel accommodation can also be found in Roskilde, though there the options are more limited. REGISTRATION The conference website will be found at: http://scandinavianlogic.weebly.com/ Details concerning registration will be posted there in due course.</pre> Erik Palmgren 2012-04-28T14:24:22 http://comments.gmane.org/gmane.science.mathematics.prooftheory/951 <pre>Dear all, I'd like to draw your attention to the fact that applications for the European Master's Program in Computational Logic are still possible UNTIL 31 May 2012. A limited number of small scholarships is available (see: http://www.emcl-study.eu/grants.html). More details are given below. Please spread this information as wide as possible among friends and colleagues, at your old universities and the places, where you currently live and work. Many thanks -- Steffen ******************************************************************** The European Master's Program in Computational Logic We are glad to announce to you the possibility to join our European Master's Program of Computational Logic. This program is offered jointly at the Free-University of Bozen-Bolzano in Italy, the Technische Universit=E4t Dresden in Germany, the Universidade Nova de Lisboa in Portugal and the Technische Universit=E4t Wien in Austria. Within this program you have the choice to study at two /three of the four European universities. In addition, you can do your project work at the National ICT of Australia (NICTA). You will graduate with a MSc in Computer Science and obtain a joint degree. Information on the universities and the program including the application procedure is provided here: http://www.emcl-study.eu/home.html Language of instruction is English. Tuition fees are 3.000 EUR (for non-European students) and 1.000 (for European students) per year. Do not hesitate to contact us if you have any further questions. Kind regards -- Steffen H=F6lldobler Prof. Dr. Steffen Hoelldobler International Center for Computational Logic Technische Universit=E4t Dresden 01062 Dresden, Germany phone: [+49](351)46 33 83 40 fax: [+49](351)46 33 83 42 email: sh-vmoGOYDZw8ZDdeZkLAqgzoQuADTiUCJX&lt; at &gt;public.gmane.org </pre> Paola Bruscoli 2012-04-25T14:39:35 http://comments.gmane.org/gmane.science.mathematics.prooftheory/950 <pre> [Apologies for multiple posting] The French ANR project LOGOI is inviting applications for a postdoctoral position within the team Logique de la Programmation (LDP) of the Institut de MathÈmatiques de Luminy (IML) in Marseille, France. Context ------- The LOGOI project pursues the programme of Geometry of Interaction (GoI), which aims at a reconstruction of logic from interaction as the primitive notion, considered as an abstract counterpart of cut elimination. This programme has started together with linear logic and has evolved since its early days, from the limited case of multiplicatives to recent developments involving the theory of operator algebras and providing a strikingly new perspective on implicit complexity via light logics. The goals of the LOGOI project are on one side to better understand and refine the current theory of GoI, and on the other side to draw on the novel tools and concepts provided by this framework, in order to propose a new structured approach to proof theory and its connections with other areas of computer science. Post Doctoral Position ---------------------- This is a full-time research position for one year, with a possible one-year extension. It is expected to start at the beginning of fall 2012 (between 1 Sep. and 1 Nov.). Research will take place at the IML in Marseille. The successful applicant will contribute to the main areas of the LOGOI project research effort: geometry of interaction, ludics, proof theoretical aspects of computation. Possible connections with other fields of proof theory and computer science are also of interest. The post-doc is of course expected to participate to group activities (workshops, meetings, tutorials) both of the LOGOI project and the LDP team. Requirements ------------ Applicants must hold a PhD degree in computer science or mathematics, and should have a strong background in logic and proof theory. Skills in an additional area of computer science (complexity, concurrency, programming language semantics, etc.) are very welcome. If the PhD thesis is not defended yet, the candidate must provide the planned defence date and the composition of the thesis committee. Knowledge of French is not required. Application ----------- To apply, please send an email to logoi-postdoc-YrJ6uwBEqj+NMqqgB3vDxg&lt; at &gt;public.gmane.org, including your current CV, a link to a list of your publications, and a research statement summarizing your research activities and goals (preferably two pages at most). You might also include the names of up to two references. The deadline for applications is 20 june 2012, but early expression of interest is encouraged. More Information ---------------- Logoi: http://www.logoi.fr/ IML: http://iml.univ-mrs.fr/ </pre> quatrini-YrJ6uwBEqj+NMqqgB3vDxg< at >public.gmane.org 2012-04-20T12:06:12 http://comments.gmane.org/gmane.science.mathematics.prooftheory/948 <pre>Please distribute this call to everybody you think intrested in. ====================================================== European PhD Program in Computational Logic (EPCL) ====================================================== http://www.epcl-study.eu/ CALL FOR APPLICATIONS The European PhD Program in Computational Logic (EPCL) is run jointly by four of the leading European universities in the field: - Free University of Bozen-Bolzano (Italy), - Technische Universität Dresden (Germany), - Technische Universität Wien (Austria), and - Universidade Nova de Lisboa (Portugal). Further international universities, research organizations and enterprises which contribute to Computational Logic or apply results from it are involved as associated partners: The Simon Fraser University (Canada), the Universidad de Chile, the National ICT Australia Limited (NICTA), and several companies. The program involves three years of PhD study in at least two of the European partner universities. It leads to a joint doctoral degree of the partner universities at which the studies have been physically performed. The language of the program is English. Financial support is available in the form of positions and scholarships. Necessary requirements for participation in EPCL are a Master's degree in Computer Science or Mathematics, or an equivalent degree; the proof of adequate knowledge of English; and substantial knowledge in the areas Foundations of Logics, Foundations of Artificial Intelligence and Declarative Programming. The program starts annually in the winter term. Applications for 2012 have to be electronically submitted on the Webpage http://www.epcl-study.eu/, before the ======================================= Application Deadline on 15 May 2012 ======================================= If you have enquiries, please do not hesitate to contact the coordinator of the program Prof. Steffen Hölldobler Technische Universität Dresden Fakultät Informatik International Center for Computational Logic Email: sh-vmoGOYDZw8ZDdeZkLAqgzoQuADTiUCJX&lt; at &gt;public.gmane.org Phone: +49 (351) 463 38340 EPCL is supported by the German Federal Ministry of Education and Research (BMBF) within the German Academic Exchange Service (DAAD) program International Doctorates in Germany (IPID). -- Dr.rer.nat.habil. Bertram Fronhöfer TU Dresden Department of Computer Science International Center for Computational Logic 01062 Dresden, Germany Tel.: +49 (0)351 463 39095 </pre> Paola Bruscoli 2012-04-19T07:46:53 http://comments.gmane.org/gmane.science.mathematics.prooftheory/947 <pre>Hello, I would like to advertise the following positions at the University of Bath. In particular we are looking for applicants in the area `Software verification and correctness´. Ciao, -Alessio Software verification and correctness We aim to build on the existing strengths within the Mathematical Foundations group in the Department of Computer Science. The group comprises Prof Guy McCusker and Dr Jim Laird (semantics), Dr Alessio Guglielmi (proof theory), Dr John Power (category theory) and Prof James Davenport (computer algebra). We seek to strengthen its activities via the appointment of a Prize Fellow in software verification &amp; correctness, to be understood broadly, to complement existing expertise; it would also be desirable to strengthen connections with other groups in the department, particularly with Dr Marina De Vos and Dr Julian Padget in the Intelligent Systems group. The Fellow would be coming into a well-resourced, lively group that runs a weekly seminar series, which once a month is jointly held with Swansea's Proofs, Complexity and Verification seminar. The Math Foundations group belongs to the Wessex Theory Seminar, comprising the Computer Science Departments of Bath, Oxford, Southampton, Cambridge, Imperial College, Queen Mary, Sussex and Swansea. The group has a good track record of nurturing early career researchers. For informal inquiries contact Prof Guy McCusker: G.A.McCusker AT bath.ac.uk ------------------------------------------------------------------------------------- Prize Fellow - Department of Computer Science Salary: Starting from £37,012, rising to £44,166 Closing Date: Monday 21 May 2012 Interview Date: See advert Reference: JK1000 To further enhance our academic base, we are making a strategic investment in recruiting University of Bath Prize Fellows across all disciplines. This is an opportunity for outstanding post-doctoral researchers to develop their academic career in a supportive and well-resourced research environment. In the Faculty of Science we will appoint a total of six Fellows to further strengthen and develop areas of existing research excellence. In the Department of Computer Science we invite applications in the areas of: * Machine Learning * Software Verification and Correctness * Modelling Behaviour Transmission Details of these priority areas and the Faculty-wide appointment process can be found here: &lt;http://www.bath.ac.uk/science/prize-fellows&gt;. The Fellows will be expected to pursue an independent programme of research, including publishing in top quality journals and securing external research grants. The initial appointment will be to a fixed-term Research Fellow post with the expectation of transfer to a permanent lectureship at the end of year two, or exceptionally at the end of year three. Applicants should upload a CV and a 2-page outline of their research plans over the next 3-5 years, showing how these complement and enhance existing research within the relevant priority area. Interviews will take place on Friday 29th June or Monday 2nd July 2012 </pre> Alessio Guglielmi 2012-04-16T17:38:58 http://comments.gmane.org/gmane.science.mathematics.prooftheory/946 <pre> *** Submission deadline extended to April 19th *** ============================================================ *** CALL FOR TALK PROPOSALS *** LOLA 2012 Syntax and Semantics of Low Level Languages Sunday 24th June 2012, Dubrovnik, Croatia A LICS 2012-affiliated workshop http://www.ccs.neu.edu/home/amal/lola2012 ============================================================ IMPORTANT DATES Submission deadline Thursday 19th April 2012 (extended) Author notification Monday 30th April 2012 Workshop Sunday 24th June 2012 SUBMISSION LINK The submissions will be made by easychair at https://www.easychair.org/conferences/?conf=lola2012 DESCRIPTION OF THE WORKSHOP It has been understood since the late 1960s that tools and structures arising in mathematical logic and proof theory can usefully be applied to the design of high level programming languages, and to the development of reasoning principles for such languages. Yet low level languages, such as machine code, and the compilation of high level languages into a low level ones have traditionally been seen as having little or no essential connection to logic. However, a fundamental discovery of this past decade has been that low level languages are also governed by logical principles. From this key observation has emerged an active and fascinating new research area at the frontier of logic and computer science. The practically-motivated design of logics reflecting the structure of low level languages (such as heaps, registers and code pointers) and low level properties of programs (such as resource usage) goes hand in hand with the some of the most advanced contemporary researches in semantics and proof theory, including classical realizability and forcing, double orthogonality, parametricity, linear logic, game semantics, uniformity, categorical semantics, explicit substitutions, abstract machines, implicit complexity and sublinear programming. The LOLA workshop, affiliated with LICS, will bring together researchers interested in many aspects of the relationship between logic and low level languages and programs. Topics of interest include, but are not limited to: Typed assembly languages, Certified assembly programming, Certified and certifying compilation, Proof-carrying code, Program optimization, Modal logic and realizability in machine code, Realizability and double orthogonality in assembly code, Parametricity, modules and existential types, General references, Kripke models and recursive types, Continuations and concurrency, Implicit complexity, sublinear programming and Turing machines, Closures and explicit substitutions, Linear logic and separation logic, Game semantics, abstract machines and hardware synthesis, Monoidal and premonoidal categories, traces and effects. SUBMISSION INFORMATION: LOLA is an informal workshop aiming at a high degree of useful interaction amongst the participants, welcoming proposals for talks on work in progress, overviews of larger programmes, position presentations and short tutorials as well as more traditional research talks describing new results. The programme committee will select the workshop presentations from submitted proposals, which may take the form either of a short abstract or of a longer (published or unpublished) paper describing completed work. PROGRAM CO-CHAIRS: Amal Ahmed (Northeastern University) Aleksandar Nanevski (IMDEA Software) PROGRAM COMMITTEE: Cristiano Calcagno (Imperial College London and Monoidics Limited) Robert Dockins (Princeton University) Martin Hofmann (LMU Munich) Xavier Leroy (INRIA Rocquencourt) Andrzej Murawski (University of Leicester) Sungwoo Park (Pohang University of Science and Technology) Dusko Pavlovic (Royal Holloway, University of London) Andreas Rossberg (Google)</pre> Amal Ahmed 2012-04-14T20:12:05 http://comments.gmane.org/gmane.science.mathematics.prooftheory/945 <pre>============================================================ *** FINAL CALL FOR TALK PROPOSALS *** LOLA 2012 Syntax and Semantics of Low Level Languages Sunday 24th June 2012, Dubrovnik, Croatia A LICS 2012-affiliated workshop http://www.ccs.neu.edu/home/amal/lola2012 ============================================================ IMPORTANT DATES Submission deadline Friday 13th April 2012 Author notification Monday 30th April 2012 Workshop Sunday 24th June 2012 SUBMISSION LINK The submissions will be made by easychair at https://www.easychair.org/conferences/?conf=lola2012 DESCRIPTION OF THE WORKSHOP It has been understood since the late 1960s that tools and structures arising in mathematical logic and proof theory can usefully be applied to the design of high level programming languages, and to the development of reasoning principles for such languages. Yet low level languages, such as machine code, and the compilation of high level languages into a low level ones have traditionally been seen as having little or no essential connection to logic. However, a fundamental discovery of this past decade has been that low level languages are also governed by logical principles. From this key observation has emerged an active and fascinating new research area at the frontier of logic and computer science. The practically-motivated design of logics reflecting the structure of low level languages (such as heaps, registers and code pointers) and low level properties of programs (such as resource usage) goes hand in hand with the some of the most advanced contemporary researches in semantics and proof theory, including classical realizability and forcing, double orthogonality, parametricity, linear logic, game semantics, uniformity, categorical semantics, explicit substitutions, abstract machines, implicit complexity and sublinear programming. The LOLA workshop, affiliated with LICS, will bring together researchers interested in many aspects of the relationship between logic and low level languages and programs. Topics of interest include, but are not limited to: Typed assembly languages, Certified assembly programming, Certified and certifying compilation, Proof-carrying code, Program optimization, Modal logic and realizability in machine code, Realizability and double orthogonality in assembly code, Parametricity, modules and existential types, General references, Kripke models and recursive types, Continuations and concurrency, Implicit complexity, sublinear programming and Turing machines, Closures and explicit substitutions, Linear logic and separation logic, Game semantics, abstract machines and hardware synthesis, Monoidal and premonoidal categories, traces and effects. SUBMISSION INFORMATION: LOLA is an informal workshop aiming at a high degree of useful interaction amongst the participants, welcoming proposals for talks on work in progress, overviews of larger programmes, position presentations and short tutorials as well as more traditional research talks describing new results. The programme committee will select the workshop presentations from submitted proposals, which may take the form either of a short abstract or of a longer (published or unpublished) paper describing completed work. PROGRAM CO-CHAIRS: Amal Ahmed (Northeastern University) Aleksandar Nanevski (IMDEA Software) PROGRAM COMMITTEE: Cristiano Calcagno (Imperial College London and Monoidics Limited) Robert Dockins (Princeton University) Martin Hofmann (LMU Munich) Xavier Leroy (INRIA Rocquencourt) Andrzej Murawski (University of Leicester) Sungwoo Park (Pohang University of Science and Technology) Dusko Pavlovic (Royal Holloway, University of London) Andreas Rossberg (Google) </pre> Amal Ahmed 2012-04-11T18:07:48 http://comments.gmane.org/gmane.science.mathematics.prooftheory/944 <pre>With apologies for duplicates. ------------------------------------------------------------------- IWS 2012 at IJCAR: CALL FOR PAPERS 2nd Joint International Workshop on Strategies in Rewriting, Proving and Programming 1 July 2012, Manchester, UK http://www.dcs.kcl.ac.uk/staff/maribel/IWS2012/IWS2012.html **** Submission: 27 April 2012 **** AIM AND TOPICS: Strategies are ubiquitous in automated reasoning engines, high level programming languages, verification tools, and affect their useability, performance and practical impact. They control search (for proofs or models), transformation (of programs), access (to resources) and modelling. Work on strategies and search plans remains often hidden in implementations of theorem provers, proof assistants, model builders, interpreters, SAT and SMT solvers, decision procedures for satisfiability, termination provers and verifiers. The 2nd IWS Workshop provides a forum to present research on strategies, focusing on the following topics: * Strategies in automated theorem provers, automated model builders, decision procedures and their combinations, SAT and SMT solvers; * Strategies and tacticals in interactive theorem provers and proof assistants; * Strategies in interpreters of programming languages, rewriting engines and termination provers; * Strategies in program analysers and tools for verification modulo theories; * Performance evaluation: empirical evaluation, comparison and optimisation of strategies; * Strategy analysis: evaluation, comparison, and optimisation of strategies by mathematical approaches to model search spaces and measure search complexity; * Strategy languages: essential constructs, meta-level features, design, implementation and application; * Applications and case studies where strategies play a major role. Papers on strategies in automated reasoning, programming languages and software verification are equally welcome, as the workshop aims at facilitating synergies. IMPORTANT DATES: All in 2012: # Submission: 27 April # Notification: 27 May # Preliminary proceedings version due: 6 June # Submission for final proceedings: 9 September # Notification: 9 November # Final version: 2 December SUBMISSION AND PUBLICATION: There are three categories of submissions: Regular: This is for typical workshop papers. Authors submit an abstract (max 5 pages). Accepted abstracts are presented at the workshop and included in the preliminary proceedings, available at the workshop. After the workshop, authors of accepted abstracts are invited to submit a full version (max 15 pages), which is refereed again for inclusion in the final workshop proceedings, to be published in EPTCS (http://eptcs.org/). Abstract-only: This is for preliminary research that may not be ready to develop into a full paper afterthe workshop. Authors submit an abstract (max 5 pages). Accepted abstracts are presented at the workshop and included only in the preliminary proceedings. Presentation-only: This is for papers in the scope of the workshop that have been or will be published elsewhere. They may be submitted in full (max 15 pages), indicating where the paper appears. If accepted, one page including title, authors, abstract as in the published paper, and a reference to the full paper, is included in the preliminary proceedings. Authors are strongly encouraged to produce their papers in LaTeX and must indicate the submission category. All submissions are through https://www.easychair.org/account/signin.cgi?conf=iws2012 also reachable from the workshop web site. PROGRAMME COMMITTEE: Maria Paola Bonacina (Co-Chair) (Universita degli Studi di Verona) Dan Dougherty, Worcester Polytechnic Institute Bruno Dutertre (SRI International) Maribel Fernandez (Co-Chair) (King's College London) Mnacho Echenim (Universite de Grenoble) Swen Jacobs (EPFL) Helene Kirchner (INRIA) Salvador Lucas (Universidad Politecnica de Valencia) Christophe Ringeissen (INRIA) Stephan Schulz (eprover.org) CONTACT: mariapaola.bonacina-2MY3Wblt4JY&lt; at &gt;public.gmane.org and Maribel.Fernandez-3vygKqVCdQxaa/9Udqfwiw&lt; at &gt;public.gmane.org </pre> Maria Paola Bonacina 2012-04-11T11:14:00 Search the mailing list at Gmane query http://search.gmane.org/?group=$group=gmane.science.mathematics.prooftheory