• News

    Look out for news e.g. new projects announcement, fundings, new PhD students and opportunities, etc.

    John Power’s visit in August

    by  • August 8, 2017 • News

    John Power is visiting HWU for 3 weeks, starting this week. He will give two talks, one at Edinburgh Informatics (15th August), and another — at HWU (16 August). See the details below. If, in the course of these weeks, you would like to meet with John, please email to me or John directly,...

    Read more →

    PhD Progression talk by Frantisek Farka, Refinement in Dependent Type Theory via Proofs by Resolution

    by  • May 30, 2017 • News

    Wednesday 31 May, 13.15, EM 1.70 — Refinement in Dependent Type Theory via Proofs by Resolution — Logic programming, that is Horn Clause Logic equipped with a resolution mechanism, provides an expressive framework for first order proving with computational advantages over alternative approaches. Traditionally, resolution mechanisms employ full unification. Recently, however, attention was given...

    Read more →

    Sven-Bodo Scholz – A λ-Calculus for Transfinite Arrays — Towards Unifying Streams and Arrays (20 April 2017)

    by  • March 14, 2017 • DSG Research Seminars: Logic and Programming Languages, News

    On Thursday the 20th April 2017 Sven-Bodo will give a PL&L seminar talk at the usual time (14:15). Arrays and streams seem to be fundamentally at odds: arrays require their size to be known in advance, streams are dynamically growing; arrays offer direct access to all of their elements, streams provide direct access to...

    Read more →

    Blesson Varghese – Scalable Computing Beyond the Cloud (30 March 2017, Thursday).

    by  • March 14, 2017 • DSG Research Seminars: Logic and Programming Languages, News

    It is forecast that over 50 billion devices will be added to the Internet by 2020. Consequently, 50 trillion gigabytes of data will be generated. Currently, applications generating data on user devices, such as smartphones, tablets and wearables use the cloud as a centralised server. This will soon become an untenable computing model. The...

    Read more →

    Yutaka Nagashima – Towards Smart Proof Search for Isabelle (13 April 2017, Thursday).

    by  • March 14, 2017 • DSG Research Seminars: Logic and Programming Languages, News

    Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this talk, I present a proof strategy language for Isabelle and a proof method recommendation tool we are developing at Data61. Then, I sketch a smart proof search tool based on these two...

    Read more →

    Spring seminars

    by  • March 9, 2017 • News

    The Spring Seminar Series are scheduled as follows (all Seminars are scheduled 14.15-15.15, on Wednesdays): 15 March 2017. Reading group. Patrick Cousot “Abstract Interpretation Based Formal Methods and Future Challenges” 22 March 2017. Jamie Gabbay, TBC 30 March 2017 (Thursday). Blesson Varghese, Queens University, Belfast. Title TBC 13 April 2017 (Thursday). Yutaka Nagashima, Trustworthy...

    Read more →