GRaDS talk: A Logic for Reasoning About LF Specifications

by Mary Southern on 2020-12-11



Reasoning is a technique used to ensure that the software we write will behave in expected and desired ways. This can take many forms, such as showing that a particular program behaves a certain way or showing some desirable property about all valid programs through reasoning about a given programming language itself. I am interested in reasoning about systems which are described using a particular language called the Edinburgh Logical Framework, or LF. This language has a type system which is more expressive than simple categorization of inputs and outputs seen in many modern programming languages, allowing it to naturally capture relations between objects of a system. My work has focused on understanding reasoning in the context of such descriptions and formalizing this reasoning by developing a logic and proof system for LF. I have further developed a theorem prover based on this logic which has been used to reason about a variety of systems. In this talk I will give an introduction to the logic and provide some insight into the challenges which have been addressed during its development. Further details will be available in my thesis.


Mary Southern is a PhD student working in Programming Languages with Gopalan Nadathur. She is interested in topics relating to Verification, Logics, and Type Theory, and is very close to completion of her degree. When not working on research she can be found skating with Minnesota Roller Derby (though not during the pandemic) or leading collaborative storytelling style role playing games.