1 citations · 1 across the 2 of their papers we have counts for
2 papers
cs.LO2021
Types are Internal -Groupoids
Antoine Allioux, Eric Finster, Matthieu Sozeau
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode…
cs.LO2017★ 1 cited
Krivine Machine and Taylor Expansion in a Non-uniform Setting
Antoine Allioux
The Krivine machine is an abstract machine implementing the linear head reduction of lambda-calculus. Ehrhard and Regnier gave a resource sensitive version returning the annotated…