[TYPES/announce] PERR 2019 CFP (extended) -- 3rd Workshop on Program Equivalence and Relational Reasoning
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [with apologies for cross-postings] == PERR 2019 3rd Workshop on Program Equivalence and Relational Reasoning A workshop at ETAPS 2019 in Prague (European Joint Conferences of Theory & Practice of Software) == Important dates: Submission deadline Fri 8 Feb 2019 (extended) Notification Fri 1 Mar 2019 Workshop Sat 6 Apr 2019 Call for Papers PERR is an annual international workshop dedicated to the formal verification of program equivalence and related relational problems. It is the 3rd in a series of meetings that bring together researchers from different areas interested in equivalence and related questions. PERR 2019 will be held as satellite workshop of ETAPS (http://www.etaps.org/). Program equivalence is arguably one of the most interesting and at the same time important problems in formal verification. It is a cross-cutting topic that has attracted the interest of several research communities: the field of denotational (game) semantics, deductive software verification, bounded model checking, specification inference, software evolution and regression testing, etc. Topics The goal of the workshop is to bring researchers of the different fields in touch and to stipulate an exchange of ideas leading to forging a community working on PERR. It welcomes contributions from the topics mentioned above but is also open to new questions regarding program equivalence. This includes related research areas of relational reasoning like program refinement or the verification of hyperproperties, in particular of secure information flow. Areas of interest include (but are not limited to): .regression verification .program equivalence .equivalence of higher order programs .product programs, relational calculi .verification of hyperproperties .program refinement, refinement calculus .specification of differences between programs .inferring semantic differences between programs .transformation validation .correct compiler transformations .automata bisimulation .code equivalence checking in teaching and marking This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tool presentations. The workshop will have informal proceedings, posted on its webpage, and speakers will be asked to consider submitting papers towards a post-proceedings volume. Submission Instructions Please submit an abstract (this can be in the form of 1-2 pages of text, or a paper of no more than 15 pages) of your proposed talk on the EasyChair submission page below. Submissions will be reviewed by at least 2 PC members and feedback will be provided. https://easychair.org/conferences/?conf=perr19 The workshop will have informal proceedings, posted on its webpage, and speakers will be asked to consider submitting papers towards an EPTCS post-proceedings volume. Program Committee Stefan Ciobaca, Alexandru Ioan Cuza University of Iasi Steve Kremer, INRIA Shuvendu K. Lahiri, Microsoft Research Xavier Leroy, Collège de France Andrzej Murawski, University of Oxford Philipp Ruemmer, Uppsala University Rahul Sharma, Microsoft Research Ofer Strichman, Technion Nikos Tzevelekos, Queen Mary University of London Mattias Ulbrich, Karlsruhe Institute of Technology Niels Voorneveld, University of Ljubljana
[TYPES/announce] PERR 2019 CFP -- 3rd Workshop on Program Equivalence and Relational Reasoning
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [with apologies for cross-postings] == PERR 2019 3rd Workshop on Program Equivalence and Relational Reasoning A workshop at ETAPS 2019 in Prague (European Joint Conferences of Theory & Practice of Software) == Important dates: Submission deadline Fri 1 Feb 2019 Notification Fri 1 Mar 2019 Workshop Sat 6 Apr 2019 Call for Papers PERR is an annual international workshop dedicated to the formal verification of program equivalence and related relational problems. It is the 3rd in a series of meetings that bring together researchers from different areas interested in equivalence and related questions. PERR 2019 will be held as satellite workshop of ETAPS (http://www.etaps.org/). Program equivalence is arguably one of the most interesting and at the same time important problems in formal verification. It is a cross-cutting topic that has attracted the interest of several research communities: the field of denotational (game) semantics, deductive software verification, bounded model checking, specification inference, software evolution and regression testing, etc. Topics The goal of the workshop is to bring researchers of the different fields in touch and to stipulate an exchange of ideas leading to forging a community working on PERR. It welcomes contributions from the topics mentioned above but is also open to new questions regarding program equivalence. This includes related research areas of relational reasoning like program refinement or the verification of hyperproperties, in particular of secure information flow. Areas of interest include (but are not limited to): .regression verification .program equivalence .equivalence of higher order programs .product programs, relational calculi .verification of hyperproperties .program refinement, refinement calculus .specification of differences between programs .inferring semantic differences between programs .transformation validation .correct compiler transformations .automata bisimulation .code equivalence checking in teaching and marking This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tool presentations. The workshop will have informal proceedings, posted on its webpage, and speakers will be asked to consider submitting papers towards a post-proceedings volume. Submission Instructions Please submit an abstract (this can be in the form of 1-2 pages of text, or a paper of no more than 15 pages) of your proposed talk on the EasyChair submission page below. Submissions will be reviewed by at least 2 PC members and feedback will be provided. https://easychair.org/conferences/?conf=perr19 The workshop will have informal proceedings, posted on its webpage, and speakers will be asked to consider submitting papers towards an EPTCS post-proceedings volume.
[TYPES/announce] HIGHLIGHTS 2017 -- Call for Participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [with apologies for multiple postings] HIGHLIGHTS 2017 -- FIFTH CONFERENCE ON HIGHLIGHTS OF LOGIC, GAMES AND AUTOMATA Call for Participation 12-15 SEPTEMBER 2017, London, UK http://highlights-conference.org * HIGHLIGHTS 2017 is the fifth conference on Highlights of Logic, Games and Automata which aims at integrating the community working in these fields. Papers from these areas are dispersed across many conferences, which makes them difficult to follow. A visit to Highlights conference should offer a wide picture of the latest research in the field and a chance to meet everybody in the community, not just those who happen to publish in one particular proceedings volume. * The program will offer 59 contributed talks, three keynotes: + Mikolaj Bojanczyk, "Recognisability equals MSO definability for graphs of bounded treewidth" + Sanjay Jain, "Quasi Polynomial and FPT algorithms for parity games" + Hung Ngo, "Shannon-type inequalities, submodular width, and disjunctive datalog" two special sessions organized by: + Patricia Bouyer, "Games played on graphs: quantitative games, games with multi-objectives, non-zero sum games" + Alexandra Silva, "Model learning, automata and its applications" and two tutorials + Veronique Cortier, "Verification of security protocols" + Damien Pous, "Coinduction up to and automata algorithms" Full programme can be found at: http://highlights-conference.org. * Registration open until August 20, 2017 at http://highlights-conference.org/register/
[TYPES/announce] HIGHLIGHTS 2017 - Call for Presentations
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Highlights of Logic, Games and Automata (HIGHLIGHTS 2017) London, 12-15 SEPTEMBER 2017 http://highlights-conference.org 1st CALL FOR PRESENTATIONS HIGHLIGHTS 2017 is the fifth conference on Highlights of Logic, Games and Automata that aims at integrating the community working in these fields. Papers from these areas are dispersed across many conferences, which makes them difficult to follow. A visit to the Highlights conference should offer a wide picture of the latest research in the field and a chance to meet everybody in the community, not just those who happen to publish in one particular proceedings volume. We encourage you to attend and present your best work, be it already published or not, at the Highlights conference. Representative areas include, but are not restricted to: logic and finite model theory, automata theory, games for logic and verification. The conference itself is three days long (Sep. 13-15) and it is preceded by the Highlights tutorial day (Sep. 12). The participation costs will be modest (with a discount for students and post-docs) and London is very easy to reach. The contributed talks are around ten minutes. Ideally, they let participants learn something new, and enable them to understand the objective/problem/question and the result, and to get an idea of the technique. The program will further offer three invited talks: + Mikolaj Bojanczyk: Recognisability equals MSO definability for graphs of bounded treewidth. + Sanjay Jain: Quasi Polynomial and FPT algorithms for parity games + Hung Ngo: Shannon-type inequalities, submodular width, and disjunctive datalog two invited sessions, organised by: + Patricia Bouyer: Games played on graphs: quantitative games, games with multi-objectives, non-zero sum games + Alexandra Silva: Model learning, automata and its applications and two tutorials: + Veronique Cortier: Verification of security protocols + Damien Pous: Coinduction up to and automata algorithms The submission deadline is *** JUNE 2, 2017*** Notifications will be sent by June 12, 2017. Registration will be possible until August 7, 2017. You submit a proposal for a presentation, not a paper. Hence, submissions should have a single author, who is the speaker. Since we expect you to present your favourite result of the year, there should be at most one submission per speaker. The abstract, of 1-2 pages, may include a list of coauthors. There are no formal proceedings and we encourage submission of work presented elsewhere. Submissions are possible through https://easychair.org/conferences/?conf=highlights17. The instructions and detailed information about Highlights 2017 are available at http://highlights-conference.org.
[TYPES/announce] Postdoc Position at Queen Mary
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are hiring one research fellow with a strong background in programming languages and verification, who can contribute to the design and implementation of a Java heterogeneous compilation tool, informed by semantic models. The deadline for applications is 08 MAY 2017. The position is for 12 months with the possibility of extension to 30 months. It is based in the School of Electronic Engineering and Computer Science, Queen Mary University of London, under the supervision of Nikos Tzevelekos, and is part of a joint project with Dan Ghica and the University of Birmingham. The project is financed by the EPSRC grant "System-Level Game Semantics: A semantic framework for composing systems”, in collaboration with external partners Aarhus University, Yale University, and Facebook. Informal inquiries can be sent to nikos.tzevele...@qmul.ac.uk. Job link: http://bit.ly/2ohUkEM Please share. Nikos Tzevelekos Senior Lecturer in Computer Science Queen Mary University of London Valuing Diversity & Committed to Equality QMUL is proud to be a London Living Wage Employer
[TYPES/announce] PhD Studentship at Queen Mary
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] PhD Studentship in Semantics and Verification of Heterogeneous Programs Applications are invited for a fully-funded PhD studentship within the Theory Group at Queen Mary University of London, as part of a project which aims to develop a unified semantic framework for heterogeneous software systems and apply it to compositional software compilation and verification. Cloud computing and heterogeneous computing are widely acknowledged to dominate the software landscape in the foreseeable future. The recent work on System-Level Games provides a semantic framework for modelling low-level code interactions involving resources shared between a program and its environment. This project will apply the framework for deriving compositional analysis techniques for the compilation and verification of heterogeneous programs. All nationalities are eligible to apply for this studentship, which will start in October 2016. The studentship is for three years, and covers student fees as well as a tax-free stipend of £16,057 per annum. Candidates must have a 2:1 degree or equivalent, and/or a good MSc Degree, in Computer Science or a related discipline. The ideal candidate should be creative and motivated in the studying of semantics and verification of programming languages. Good coding skills will be an advantage, and applicants will have at least good knowledge of programming languages such as C/C++, Java, Python, OCaml. Analytical and good communication skills are also welcome. The PhD supervisor will be Dr Nikos Tzevelekos. The project will be based in the School of Electronic Engineering and Computer Science (EECS), and the student will join a world-leading centre for research on logical methods for reasoning about computer systems in the Theory Group (http://theory.eecs.qmul.ac.uk/). The position will be integrated in the EPSRC project "System-Level Game Semantics: A unifying framework for composing systems", which is in collaboration with the University of Birmingham. Informal enquiries about the studentship can be made by email to Dr Tzevelekos (nikos.tzevele...@qmul.ac.uk). To apply, please follow the on-line process at www.qmul.ac.uk/postgraduate/applyresearchdegrees/ click on the list of Research Degree Subjects, select "Computer Science", and follow the instructions on the right-hand side of the web page. Please note that instead of the Research Proposal we request a Statement of Research Interests. Your statement should answer two questions: (i) Why are you interested in the topic described above? (ii) What relevant experience do you have? Your statement should be brief: no more than 500 words or one side of A4 paper. In addition we would also like you to send a sample of your written work (e.g. excerpt of final year dissertation or published academic paper). More details can be found at: http://www.eecs.qmul.ac.uk/phd/how-to-apply The closing date for the applications is 24/07/2016. Interviews are expected to take place the week of 25 July 2016.
[TYPES/announce] Postdoc at Queen Mary University of London (semantics and verification)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Postdoctoral Research Assistant School of Electronic Engineering and Computer Science Queen Mary University of London Duration: 16 months Salary: £31,113 - £34,626 pa Deadline: 17 May 2014 Applications are invited for a postdoctoral position in the area of semantics-based software verification, on the EPSRC-funded project Program Reasoning with Nominal Game Semantics. We are looking for candidates with a strong background in programming language semantics and/or topics in verification, who can contribute to the design and implementation of program logics for higher-order programs. The project will be led by Nikos Tzevelekos. Other members of the School at Queen Mary working on related topics include Dino Distefano, Pasquale Malacaria, Michael Tautschnig and Greta Yorsh. The official advert can be found at http://www.jobs.qmul.ac.uk/4740 Informal enquiries are very welcome.
[TYPES/announce] GALOP 2013 - Call for Participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] == *** CALL FOR PARTICIPATION *** GaLoP VIII 8th Workshop on Games for Logic and Programming Languages 18-19 July 2013, Queen Mary, University of London, UK http://www.gamesemantics.org/galop-viii == We are pleased to announce the details of this year's GaLoP workshop. REGISTRATION There is no registration fee for attendance at this informal workshop. However, participants are asked to register by sending an email to nik...@eecs.qmul.ac.uk. INVITED SPEAKERS Ichiro Hasuo, Tokyo Colin Stirling, Edinburgh Viktor Winschel, Mannheim Nobuko Yoshida, Imperial PROGRAMME Thursday 18th July 10:00-11:15: coffee and arrivals 11:15-12:30: INVITED TALK - Nobuko Yoshida: Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types Raymond Hu, Rumyena Neyova and Nobuko Yoshida: Multiparty session types and their application in large distributed systems 12:30-14:00: lunch 14:00-15:15: INVITED TALK - Colin Stirling: Introduction to decidability of higher-order matching Valentin Blot: Realizability for Peano Arithmetic with Winning Conditions in HO Games 15:15-15:45: coffee 15:45-17:00: INVITED TALK - Viktor Winschel: A Coalgebraic Framework for Games in Economics (joint work with Achim Blumensath) Jules Hedges: Sequential and simultaneous games with selection functions Friday 19th July 09:00-10:30: Julian Gutierrez and Michael Wooldridge: Equilibria in Games on Event Structures Cai Wingfield, Guy McCusker and John Power: Graphical Foundations for Dialogue Games Paul Blain Levy: Morphisms between plays 10:30-11:00: coffee 11:00-12:15 INVITED TALK - Ichiro Hasuo: Categorical GoI for Higher-Order Quantum Computation Ugo Dal Lago and Margherita Zorzi: Wave-Style Token Machines and Quantum Lambda Calculi 12:15-14:00: lunch 14:00-15:00 Dan Ghica and Olle Fredriksson: Game Semantics for Abstract Machines, revisited Alex I. Smith: A Tag-Based Approach to Syntactic Control of Interference 15:00-15:30: coffee 15:30-16:30 James Laird: Games for Model-Checking Generic Polymorphism Andrzej Murawski and Nikos Tzevelekos: Deconstructing general references via game semantics 16:30-17:00: Wrapping up LOCAL INFORMATIOM Available at http://www.gamesemantics.org/galop-viii/local-information ORGANIZING COMMITTEE Organising co-chairs: Guy McCusker, Bath Nikos Tzevelekos, QMUL Program committee: Ugo Dal Lago, Bologna Dan Ghica, Birmingham Juha Kontinen, Helsinki Guy McCusker, Bath (co-chair) Andrzej Murawski, Warwick Nikos Tzevelekos, QMUL (co-chair) Glynn Winskel, Cambridge
[TYPES/announce] GALOP 2013 - Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] 8th Workshop on Games for Logic and Programming Languages (GaLoP 2013) // Queen Mary, University of London // London, UK // 18-19 July // http://www.gamesemantics.org [apologies for possible cross-postings] GaLoP is an annual international workshop on game-semantic models for logics and programming languages and their applications. This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tutorials as well as contributed papers and invited talks. GaLoP VIII will be held in London, UK, on 18-19 July 2013. It will be a stand-alone workshop hosted at the Mile End campus of Queen Mary, University of London. Contributions are invited on all pertinent subjects, with particular interest in game-semantic and interaction models for logics and programming languages, and applications to program analysis. Typical but not exclusive areas of interest are: * Game theory and interaction models in semantics; * Games-based program analysis and verification; * Logics for games and games for logics; * Algorithmic aspects of games; * Categorical aspects; * Programming languages and full abstraction; * Higher-order automata and Petri nets; * Geometry of interaction; * Ludics; * Epistemic game theory; * Logics of dependence and independence; * Computational linguistics. There will be no formal proceedings but the possibility of a special issue in a journal will be considered (the 2005, 2008 and 2011 workshops led to special issues in Annals of Pure and Applied Logic). // Submission Instructions // Please submit an abstract of your proposed talk on the easychair submission page below. You may also submit an accompanying paper for the talk. https://www.easychair.org/conferences/?conf=galop2013 // Important Dates // Submission: May 31 Notification: June 7 Workshop: July 18-19 // Invited speakers // • Ichiro Hasuo, Tokyo • Colin Stirling, Edinburgh • Viktor Winschel, Mannheim • Nobuko Yoshida, Imperial // Program Committee // • Ugo Dal Lago, Bologna • Dan Ghica, Birmingham • Juha Kontinen, Helsinki • Guy McCusker, Bath (co-chair) • Andrzej Murawski, Warwick • Nikos Tzevelekos, QMUL (co-chair) • Glynn Winskel, Cambridge
[TYPES/announce] 17th Wessex theory seminar - Call for Participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies for multiple postings.] The 17th Wessex theory seminar will take place on Thursday 20 September at Queen Mary, University of London. As usual there is some funding available from the London Mathematical Society to support attendance. There is no registration fee, but it would be useful if you contacted us if planning to attend. Confirmed speakers are: - Nobuko Yoshida (Imperial), Multiparty Session Automata and their application in large distributed systems. - Stefan Kiefer (Oxford), On the equivalence problem for probabilistic automata. - Tony Tan (Edinburgh/Warsaw), An Automata Model for Trees with Ordered Data Values. - Radu Grigore (Queen Mary), Register Automata and Java. - Jules Villard (UCL), The Ramifications of Sharing in Data Structures. Further information on location, schedule, speakers, etc. can be found at the website: http://wiki.bath.ac.uk/display/wessex/17th+Wessex+Theory+Seminar Best wishes, Nikos Tzevelekos Edmund Robinson
