PLP Un interpretor realizat în Coq (realizat la laboratoarele de la Principii ale limbajelor de programare).