Coinducția în informatică este o metodă pentru determinarea și demonstrarea proprietăților sistemelor de obiecte care interacționează paralel (în general). Din punct de vedere matematic, este dual cu inducția structurală .
Ca definiție sau specificație , coinducția descrie o metodă prin care un obiect poate fi descompus în obiecte mai simple. Ca tehnică de demonstrare matematică, coinducția poate fi folosită pentru a arăta că toate cerințele prevăzute de specificație sunt satisfăcătoare pentru un nume de cod .
În programare, paradigma ecologică este o extensie naturală a programării logice și a coinducției care generalizează și alte extensii ale programării logice, cum ar fi copaci infiniti , predicate leneși și predicate care interacționează paralel. Programarea ecologică are aplicații în domeniile arborilor raționali, dovedind proprietăți infinite, evaluare leneșă, inferență paralelă, verificare model etc.
Codata este o entitate duală la date . Codata sunt containere potențial infinite care pot conține atât date, cât și elemente de date de cod. Mecanismul de corecursie este utilizat pentru a opera cu codata, coinducția este folosită pentru a demonstra proprietățile codatei (în analogie directă cu datele, pentru care se utilizează recursiunea și , respectiv, inducția ).