Projects per year
Abstract
ML4PG is a machinelearning extension that provides statistical proof hints during the process of Coq/SSReflect proof development. In this paper, we use ML4PG to find proof patterns in the CoqEAL library  a library that was devised to verify the correctness of Computer Algebra algorithms. In particular, we use ML4PG to help us in the formalisation of an efficient algorithm to compute the inverse of triangular matrices.
Original language  English 

Title of host publication  Intelligent Computer Mathematics 
Subtitle of host publication  MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 812, 2013. Proceedings 
Editors  Jacques Carette, David Aspinall , Christoph Lange, Petr Sojka, Wolfgang Windsteiger 
Place of Publication  Berlin 
Publisher  Springer 
Pages  354358 
Number of pages  5 
ISBN (Electronic)  9783642393204 
ISBN (Print)  9783642393198 
DOIs  
Publication status  Published  2013 
Event  Conferences on Intelligent Computer Mathematics: Calculemus 2013  University of Bath in Building 8W, Bath, United Kingdom Duration: 8 Jul 2013 → 12 Jul 2013 http://www.cicmconference.org/2013/cicm.php 
Publication series
Name  Lecture notes in computer science 

Publisher  Springer 
Volume  7961 
ISSN (Print)  03029743 
Conference
Conference  Conferences on Intelligent Computer Mathematics: Calculemus 2013 

Abbreviated title  CICM 2013 
Country  United Kingdom 
City  Bath 
Period  8/07/13 → 12/07/13 
Other  Held as Part of CICM 2013 
Internet address 
Fingerprint Dive into the research topics of 'ML4PG in computer algebra verification'. Together they form a unique fingerprint.
Projects
 1 Finished

Coalgebraic Logic Programming for Type Inference: Parallelism and Corecursion for New Generation of Programming Languages (Joint with the University of Bath)
Komendantskaya, E.
Engineering and Physical Sciences Research Council
1/09/13 → 31/01/17
Project: Research
Research output

Machine learning in Proof General: interfacing interfaces
Komendantskaya, E., Heras, J. & Grov, G., 2013, In: Electronic Proceedings in Theoretical Computer Science. 118, p. 1541 26 p.Research output: Contribution to journal › Article › peerreview

ML4PG in computer algebra verification
Heras, J. & Komendantskaya, E., 2013.Research output: Contribution to conference › Other
Activities
 2 Participation in conference

Conferences on Intelligent Computer Mathematics: Calculemus 2013
Katya Komendantskaya (Participant)
9 Jul 2013Activity: Participating in or organising an event types › Participation in conference

Conferences on Intelligent Computer Mathematics: Calculemus 2013
Jonathan Heras (Member of programme committee)
8 Jul 2013 → 12 Jul 2013Activity: Participating in or organising an event types › Participation in conference