Why has there been so much activity and excitement around the fish tank this week?
Baby Cichlids have been spotted hiding amongst the rocks. Let’s hope they grow large enough, not be eaten, when they make a bid for freedom.
Photographing the camera shy proved rather tricky. Masih finally succeeded this morning.
Thirty five years ago computers made a dramatic debut in mathematics with the famous proof of the Four Color Theorem by Appel and Haken. Their role has been expanding recently, from computational devices to tools that can tackle deduction and proofs too complex for (most) human minds, such as the Kepler conjecture or the Classification of Finite Simple Groups.
These new “machine” proofs entail fundamental changes in the practice of mathematics: a shift from craftsmanship, where each argument is a tribute to the ingenuity of the mathematician that perfected it, to a form of engineering where proofs are created more systematically. In addition to formal definitions and theorems, mathematical theories also contain clever, context-sensitive notations, usage conventions, and proof methods. To mechanize advanced mathematical results it is essential to capture these more informal elements, replacing informal and flexible usage conventions with rigorous interfaces, and exercise apprenticeship with precise algorithms. This can be difficult, requiring an array of techniques closer to software engineering than formal logic, but it is essential to obtaining formal proofs of graduate-level mathematics, and can give new insight as well.
In this talk we will give several examples of such empirical formal mathematics that we have encountered in the process of mechanizing a large corpus of Combinatorics and Algebra required by the proofs of the Four Colour and Odd Order Theorem.
Bio:Georges Gonthier is a Principal Researcher at Microsoft Research Cambridge. Dr. Gonthier has worked on the Esterel reactive programming language, techniques for the optimal computation of functional programs, the design and formal verification of a concurrent garbage collector, the join calculus model of concurrency, concurrency analysis of the Ariane 5 flight software, using full abstraction in the analysis of security properties, and a fully computer-checked proof of the famous Four Colour Theorem. He now heads the Mathematical Components project at the MSR Inria Joint Center, following up on the latter work with the development of a comprehensive library of formalized abstract algebra.
Georges Gonthier – Head of the Mathematical Components team Microsoft Research-INRIA joint centre http://www.msr-inria.inria.fr/
There will be bisquits from 3:45 downstairs
November 2002, and plans were unveiled in the university news, for a new Computer Science Building. Stages of the build were photographed for posterity.
An electronic voting system, developed by Ross and Stuart, was used to conduct the election for the new Rector. Full results are available in the University News.
Fehmi and Tristan’s paper, Context-based Personalised Settings for Mobile Location Sharing, featured in the PeMA 2011: Personalization in Mobile Applications Workshop.
The 5th ACM International Conference on Recommender Systems, took place in Chicago, Illinois from the 23rd until the 27th October.
Work carried out by Mary Steele, Titilayo Adegbamiye (both supervised by Gordon) and Shangyi Jiang (supervised by Ishbel), in fulfilment of their MSc, has continued success.
Mary’s dissertation focus, promoting public awareness of the links between lifestyle and cancer A controlled study of the usability of health information leaflets, has been accepted for publication in the International Journal of Medical Informatics.
Titilayo’s disssertation focus, evaluating the Usability of Home Blood Pressure Monitors, featured in Workshop Proceedings at INTERACT 2011. Final proceedings are now available.
Charlie’s (Shangyi Jiang) focus on virtual worlds contributed to Ishbel’s Paper, A taxonomy of virtual worlds usage in education, recently accepted by the British Journal of Educational Technology.
The School holds monthly information meetings for staff.
Another successful and well-attended Wednesday visiting day took place yesterday. Prospective undergraduates had the opportunity to meet staff, current students, eat cake and view the School facilities.
The familiar but extremely useful events are organised by Tristan, Adam and Saleem with help from volunteer students.
Isabel, Jesal, Anastasia and Thomas were the student volunteers undertaking yesterday’s tour and answering general questions.
Life in the Comp Sci Labs
The MSc lab in the John Honey building was busy with IT students holding initial group work meetings, for their next assignment. The advanced network students were networking, in a virtual sense, using WI-FI island.
Yemliha and Umer looked occupied in the HCI lab. A number of 3rd and 4th year students were busy with Project work in The Honours lab. Alas Davie and Jim were busy elsewhere.
Attendance in the 1st and 2nd year sub-honours lab, in the Jack Cole building, could be indicative of an imminent deadline. Modelling of various persuasions appeared to be the focus.
Colin and Alan’s paper, The Third Dimension in Open Learning will feature in the T2E Technical Session Engineering Frontiers of Instructional Technologies, today.
The Frontiers in Education Conference taking place in South Dakota has become the premiere conference for innovative curricula made possible by three sponsoring professional societies. ASEE Educational Research and Methods Division, IEEE Education Society and IEEE Computer Society.
