IMDEA Software

IMDEA initiative

Home > Events > Invited Talks > 2019 > Proof-Relevant Resolution: The Foundations of Constructive Automation

František Farka

Tuesday, April 30, 2019

10:45am Meeting room 302 (Mountain View), level 3

František Farka, PhD Student, Heriot-Watt University, United Kingdom

Proof-Relevant Resolution: The Foundations of Constructive Automation


In this talk, we introduce proof-relevant resolution, a framework for constructive proof automation. The intended application of the framework is verifiable proof automation in strongly typed programming languages. We motivate the framework by two use-cases that show its strengths. First, we show a proof-relevant approach to type inference and term synthesis. Secondly, we demonstrate the use of the framework for the purpose of study semantical properties of programming languages, namely soundness of type-class elaboration.

In the talk, we describe the key features of big-step and small-step operational semantics and show soundness of the small-step w.r.t. the big-step semantics. We briefly outline the proof as it requires a use of logical relation. We conclude the talk by a discussion of future applications and extensions of the framework.