• DSG Research Seminars: Logic and Programming Languages

    The Spring Seminar Series are scheduled on Wednesdays at 14.15-15.15 unless otherwise stated.
    For details please see the Spring Seminar Series page.

    John Power – Category theoretic semantics for theorem proving in logic programming: embracing the laxness (16 August, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    A propositional logic program P may be identified with a P_fP_f-coalgebra on the set of atomic propositions in the program. The corresponding C(P_fP_f)-coalgebra, where C(P_fP_f) is the cofree comonad on P_fP_f, describes derivations by resolution. That correspondence has been developed to model first-order programs in two ways, with lax semantics and saturated semantics, based...

    Read more →

    Ilya Sergey – Programming and Proving with Distributed Protocols (26 July, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    Distributed systems play a crucial role in modern infrastructure, but are notoriously difficult to implement correctly. This difficulty arises from two main challenges: (a) correctly implementing core system components (e.g., two-phase commit), so all their internal invariants hold, and (b) correctly composing standalone system components into functioning trustworthy applications (e.g., persistent storage built on...

    Read more →

    David Janin – Programing with inverse semigroups : the turtle, its pen and its violin (5 July, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    Logo is an educational programming language, designed in 1967, that is often known for its use of Turtle graphics, in which commands for movement and drawing produce line graphics either on screen or with a small robot called a turtle. In this talk, I will show how basic semigroup theoretical concepts, such as semigroup...

    Read more →

    Laura Ciobanu Radomirovic – The language complexity of solutions of equations in free semigroups and groups (21 June, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    We show that, given a word equation over a finitely generated free group (or semigroup), the set of all solutions in reduced words forms an EDT0L language. In particular, it is an indexed language in the sense of Aho. This is joint work with Murray Elder and Volker Diekert.

    Read more →

    Yutaka Nagashima – Towards Smart Proof Search for Isabelle (7 June, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    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 →

    Frantisek Farka – Refinement in Dependent Type Theory via Proofs by Resolution (31 May, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    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 to type-theoretic interpretation of logic programming with the focus on universal fragment of Horn Clause Logic where...

    Read more →

    Yue Li – Productive Corecursion in Logic Programming (10 May, 2017)

    by  • September 8, 2017 • DSG Research Seminars: Logic and Programming Languages

    Logic Programming is a Turing complete language. As a consequence, designing algorithms that decide termination and non-termination of programs or decide inductive/coinductive soundness of formulae is a challenging task. For example, the existing state-of-the-art algorithms can only semi-decide coinductive soundness of queries in logic programming for regular formulae. Another, less famous, but equally fundamental...

    Read more →

    Rob Stewart – High Level DSLs for Performance Portability! Are there DSLs? (3rd May 2017)

    by  • April 12, 2017 • DSG Research Seminars: Logic and Programming Languages

    This talk will be on 26th April, at the time of 13:15. HPC, GPU and FPGA programmers today often choose relatively low level programming languages such as CUDA, OpenCL, MPI and C, in the belief that direct control of memory management and thread scheduling is the best approach for high performance. An important disadvantage...

    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 →