6 citations · 9 across the 5 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
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…
cs.LO2021
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…
cs.LO2016★ 2 cited
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…