Invited Speakers Women in Logic 2018
Title: Logic and software engineering: are we nearly there yet?
Abstract:
Logic has been acknowledged as potentially important to software
engineering for as long as the latter field has existed. Yet, in practice,
most software today is built without explicit reliance on logic, and often
by people who do not think of themselves as having any knowledge of formal
logic. I will claim that this is unlikely to change. Does that mean logic
is not useful to software engineering? Of course not: but it means its role
may be implicit more than explicit, or concealed in language and tool
design. I will discuss some of the ways I have seen logic turn up in
model-driven software development, in particular, and try to point out some
interesting challenges for the future.
MiniBio: Perdita Stevens is Professor of Mathematics of Software Engineering in the
Laboratory for Foundations of Computer Science at the University of
Edinburgh. Her work on bidirectional transformations ultimately aims to
revolutionise software development by moving decisions away from software
specialists towards users.
Title: POPLMark Reloaded: Mechanizing Logical Relations Proofs
Abstract:
Mechanizing formal systems, given via axioms and inference rules,
together with proofs about them plays an important role in
establishing trust in formal developments. Over the past decade, the
POPLMark challenge popularized the use of proof assistants in
mechanizing the metatheory of programming languages. Focusing on the
the meta-theory of System F with subtyping, it allowed the programming
languages community to survey existing techniques to represent and
reason about syntactic structures with binders and promote the use of
proof assistants. Today, mechanizing proofs is a stable fixture in the
daily life of programming languages researchers.
As a follow-up to the POPLMark Challenge, we propose a new collection of
benchmarks that use proofs by logical relations. Such proofs are now used to attack
problems in the theory of complex languages models, with applications
to issues in equivalence of programs, compiler correctness,
representation independence and even more intensional properties such
as non-interference, differential privacy and secure multi-language
inter-operability. Yet, they remain challenging to mechanize.
In this talk, we focus on one particular challenge problem, namely
strong normalization of a simply-typed lambda-calculus with a proof by
Kripke-style logical relations. We will advocate a modern view of this
well-understood problem by formulating our logical relation on
well-typed terms. Using this case study, we share some of the lessons
learned tackling this challenge problem in Beluga, a proof environment
that supports higher-order abstract syntax encodings, first-class
context and first-class substitutions. We also discuss and highlight
similarities, strategies, and limitations in other proof assistants
when tackling this challenge problem.
We hope others will be motivated to submit solutions! The goal of this
talk is to engage the community in discussions on what support in
proof environments is needed to truly bring mechanized metatheory to
the masses.
This is joint work with Andreas Abel (Chalmers), Aliya Hameer (McGill),
Alberto Momigliano (Univ. of Milan), Steven Schäfer (Univ. Saarbrücken),
Kathrin Stark (Univ. Saarbrücken)
MiniBio: Brigitte Pientka is an Associate Professor in the School of Computer Science
at McGill University, Montreal, Canada.
Currently she is a Humboldt Research Fellow at the Ludwig Maximilian University Munich, Germany.
She received her Ph.D. from Carnegie Mellon University (USA). Her research interest lies in developing a
theoretical and practical foundation for building and reasoning about reliable safe software systems.
To achieve this goal, she combines theoretical research on the logical foundations of computer science
in programming languages and verification with system building.