Forcing in Coq

A plugin for Coq that implements a generic Forcing translation for any given set of conditions. Includes an example of a step-indexed model of pure lambda calculus.

Data and Resources

Additional Info

Field Value
Source https://inria.hal.science/hal-00767483
Author Sozeau, Matthieu, Tabareau, Nicolas, Jaber, Guilhem
Maintainer CCSD
Last Updated May 30, 2026, 00:14 (UTC)
Created May 30, 2026, 00:14 (UTC)
Identifier hal-00767483
Language en
contributor Design, study and implementation of languages for proofs and programs (PI.R2) ; Preuves, Programmes et Systèmes (PPS) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
creator Sozeau, Matthieu
date 2012-09-14T00:00:00
harvest_object_id 23126019-55be-4a85-96c7-c2c6576fbd49
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2026-01-26T00:00:00
set_spec type:OTHER