Cerise.moe

Logique

Discipline maîtresse des maths, difficilement approchable

Théorie des modèles

Catégoricité de Morley

Théorie de la preuve

PA2

Hiérarchie logique Théorème de Hedberg

ZFC

Doutes sur remplacement, powerset, choix On parle de AD Cardinaux Mahlö ?

Lambda-calcul

Théorème de Böhm Sémantique dans les domaines

STLC et typages simples

Hindley-Milner, GADT, typeclasses

Système F

Candidats de réducibilité, paramétricité, imprédicativité

MLTT

Types inductifs, inductifs-inductifs, types coinductifs, univers Divers axiomes : funext, propext, K

HoTT

Univalence, HITs

Types intersections

Typabilité = normalisation

Logique linéaire

Catégories *-autonomes

Forcing

Forcing en topos, forcing dans les ensembles, forcing en calculabilité, forcing en réalisabilité

Réalisabilité

Topos effectifs