Chuck Liang visited the team during the week of 16 December. He gave a talk on Wednesday 18 Dec.
Dec 20
PhD defense of Mahfuza Farooque
Mahfuza Farooque succeesfully defended her PhD yesterday (19 Dec 2013). Her thesis is titled “Automated reasoning techniques in sequent calculus”.
Dec 02
Danko Ilik begins his postdoc in Parsifal
Danko Ilik starts a one year postdoc within the team. He will be part of the ProofCert effort.
Nov 13
Internships for 2014 available
Members of Parsifal have posted internships for 2014 (M2 level).
Oct 15
PhD defense of Ivan Gazeau
Ivan Gazeau succeesfully defended his PhD yesterday (14 Oct 2013). His thesis is titled “Safe Programming in finite precision: Controling the errors and information leaks”. Ivan is in the process of packing up and moving to his next position as a PostDoc researcher at the University of Birmingham.
Aug 30
Accepted paper at CPP 2013
Jul 21
Abella 2.0.0 released
After over a year of development, Abella 2.0.0 has been released! The new release removes all the arbitrary restrictions on the specification logic, which is now fully higher-order. As a result, this version of Abella allows backchaining in specification contexts, and therefore also supports inductive specifications of dynamic extensions of programs. This example characterizing equivalence-upto-β via paths illustrates the use of reasoning on higher-order contexts.
Much of the development of this release has been done by Yuting Wang during his internship at Parsifal as part of the RAPT Associated Team. Other major contributors to this release include Kaustuv Chaudhuri (Parsifal) and Andrew Gacek (Rockwell Collins, USA).
For the logicians, the new extensions of Abella are documented in the following paper to appear at PPDP 2013 later this year:
- Y. Wang, K. Chaudhuri, A. Gacek, and G. Nadathur, Reasoning about Higher-Order Relational Specifications, to appear at PPDP 2013, September 2013
Jul 15
Accepted paper at LFMTP 2013
A paper by Mahfuza Farooque, Stéphane Graham-Lengrand, and Assia Mahboubi titled A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus has been accepted to LFMTP 2013 and will be presented at the workshop in Boston during September 2013.
Jun 24
Elaine Pimentel and Carlos Olarte visiting until 16 July
Prof. Elaine Pimentel (UFMG) and Prof. Carlos Olarte (Univ. Javeriana, Cali) are visiting Parsifal and Comète in June and July.
May 21
Chuck Liang and Gopalan Nadathur visit Parsifal in May
Prof. Chuck Liang (Hofstra) and Prof. Gopalan Nadathur (Univ. Minnesota) are visiting Parsifal during May and June. Chuck will be here until 15 June and Gopalan until 31 May.
