Introduction A taste of forcing Higher order arithmetic tuned The forcing transformation The forcing machine Conclusion

Niveau: Supérieur
Introduction A taste of forcing Higher-order arithmetic (tuned) The forcing transformation The forcing machine Conclusion A computational analysis of the proof transformation by forcing Alexandre Miquel June 22th, 2010 – TypiCal seminar – Ecole polytechnique

• ¬¬-translation cps


• classical realizability


• study underlying program


• program transform


• realizability generalizes standard


• transform stack


• forcing