Publications (6)
Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints
Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens +3
Type annotations are essential when printing terms in a way that preserves their meaning under reparsing and type inference. We study the problem of complete and minimal type annot…
Foundational Extensible Corecursion
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is…
Efficient Evaluation of Arbitrary Relational Calculus Queries
Martin Raszyk, David Basin, SrÄan KrstiÄ +1
The relational calculus (RC) is a concise, declarative query language. However, existing RC query evaluation approaches are inefficient and often deviate from established algorithm…
Formal Languages, Formally and Coinductively
Dmitriy Traytel
Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branchi…
A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)
César Sánchez, Gerardo Schneider, Wolfgang Ahrendt +13
Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime…
Quotients of Bounded Natural Functors
Basil Fürer, Andreas Lochbihler, Joshua Schneider +1
The functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL). For example, inductive and coinductive datatyp…