17 citations · 77 across the 28 of their papers we have counts for
Showing 2017Show all
2 papers · 1 filter
cs.PL2017★ 5 cited
From Reversible Programs to Univalent Universes and Back
Jacques Carette, Chao-Hong Chen, Vikraman Choudhury +1
We establish a close connection between a reversible programming language based on type isomorphisms and a formally presented univalent universe. The correspondence relates combina…
cs.LO2017
Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study
Jacques Carette, William M. Farmer
A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for formalizing algori…