1 citations · 1 across the 2 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2010★ 1 cited
Controlling program extraction in Elementary Linear Logic
Marc Lasson
We present an adaptation, based on program extraction in elementary linear logic, of Krivine & Leivant's system FA_2. This system allows to write higher-order equations in order to…
cs.LO2010
Internalized realizability in pure type systems
Marc Lasson
Let P be any pure type system, we are going to show how we can extend P into a PTS P' which will be used as a proof system whose formulas express properties about sets of terms of…