@ FII

Laborator: Type Systems

Citiți cu atenție sistemul de tipuri definit pentru expresii discutat la curs. Rulați din nou exemplele și demonstrațiile discutate.
Mai departe, pentru seria de exerciții propuse se consideră cunoscută următoarea sintaxa BNF a unui limbaj de expresii:

E ::= 'O' | 'S' E | 'isZero' E | 'T' | 'F' | 'ite' E E E

Cerință: Definiți aceasta sintaxă în Coq.

(1 punct) Definiți o semantică Small-Step pentru expresiile E de mai sus.
(2 puncte) Scrieți (în ASCII) regulile de tipizare pentru expresiile de mai sus.

Exemplu:

           .
TZero ------------
        O : Nat

         e : Nat
TSucc -------------
        S e : Nat

Se acordă câte 0.5 puncte pentru fiecare regulă scrisă corect pentru celelalte construcții din E rămase: isZero E, T, F, ite E E E.

(2 puncte) Scrieți (în ASCII, ca mai sus) și implementați în Coq 2 exemple de derivări care utilizează regulile de tipizare pe care le-ați definit la exercițiul 2. Cele 2 exemple trebuie să acopere toate construcțiile limbajului de expresii E. Testați implementarea fără a folosi eauto.

Se acordă câte 1 punct pentru fiecare derivare corectă, doar în condițiile în care toate regulile sunt utilizate cel puțin o singură dată.

(4 puncte) Demonstrați proprietățile: progress (2 puncte), type preservation (1 punct) și type soundness (1 punct) pentru sistemul de tipuri asociat limbajului de expresii.