-
Extracting Herbrand trees from Coq
Software certification aims at proving the correctness of programs but in many cases, the use of external libraries allows only a conditional proof: it depends on the... -
A simple presentation of the effective topos
We propose for the Effective Topos an alternative construction: a realisability framework composed of two levels of abstraction. This construction simplifies the proof...
