3 citations · 3 across the 5 of their papers we have counts for
5 papers
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…
Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model
Kevin Kappelmann, Fabian Huch, Lukas Stevens +1
We present a semi-automated framework to construct and reason about programs in a deeply-embedded while-language. The while-language we consider is a simple computation model that…
Zippy -- Generic White-Box Proof Search with Zippers
Kevin Kappelmann
We present a framework for tree-based proof search, called Zippy. Unlike existing proof search tools, Zippy is largely independent of concrete search tree representations, search-a…
Transport via Partial Galois Connections and Equivalences
Kevin Kappelmann
Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations m…
Engaging, Large-Scale Functional Programming Education in Physical and Virtual Space
Kevin Kappelmann, Jonas Rädle, Lukas Stevens
Worldwide, computer science departments have experienced a dramatic increase in the number of student enrolments. Moreover, the ongoing COVID-19 pandemic requires institutions to r…