9 citations · 26 across the 9 of their papers we have counts for
3 papers · 1 filter
From signatures to monads in UniMath
Benedikt Ahrens, Ralph Matthes, Anders Mörtberg
The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core depend…
Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
José Espírito Santo, Ralph Matthes, Luís Pinto
A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting…
A Coinductive Approach to Proof Search through Typed Lambda-Calculi
José Espírito Santo, Ralph Matthes, Luís Pinto
In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inferen…