AI4FM / 2014

A satellite workshop of ITP 2013, Rennes, France, 22nd July 2013

  • 9:00: Invited Talk: Sharing the Burden of (Dis)proof with Nitpick and SledgehammerJasmin Blanchette
  • 10:00: Coffee
  • 10:30: The social machine of mathematicsUrsula Martin
  • 11:00: Verifying the heap: an AI4FM case study Leo Freitas, Cliff Jones, Andrius Velykis and Iain Whiteside
  • 11:30: Applying machine learning to setting time limits on decision procedure callsZongyan Huang and Lawrence Paulson
  • 12:00: Lunch
  • 2:30: Arís: Analogical Reasoning for reuse of Implementation & Specification Mihai Pitu, Daniela Grijincu, Peihan Li, Asif Saleem, Rosemary Monahan, Diarmuid O’Donoghue
    • 2:30: Source Code Matching for reuse of Formal Specifications Daniela Grijincu
    • 3:00: Source Code Retrieval using Case Based Reasoning Mihai Pitu
  • 3:30 Learning Domain-Specific Guidance for Theory FormationJeremy Gow
  • 4:00: Coffee
  • 4:30: Drawing Proof StrategiesGudmund Grov
  • 5:00: Analogical Lemma Speculation Ewen Maclean
  • 5:30: Theory Exploration for Interactive Theorem ProvingMoa Johansson
  • 6:00: End of Workshop
The proceedings of the workshop have been published as a technical report accessible from the Heriot-Watt Technical Report Series here. Alternatively download the proceedings directly here.