@ FII

Laborator 8

• Back to PLP - Fall 2022
• Type systems

Exerciții de antrenament:

• Citiți cu atenție sistemul de tipuri definit pentru expresii discutat la curs. Rulați din nou exemplele și demonstrațiile discutate.

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

1. (1 punct) Definiți o semantică Small-Step pentru expresiile de mai sus.

2. (2 puncte) Scrieți (în ASCII) regulile de tipizare pentru expresiile de mai sus. Exemplu:

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

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

3. (2 puncte) Scrieți (în ASCII, ca mai sus) 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.

4. (2 puncte) Implementați regulile de la exercițiul 2 în Coq și testați implementarea pe exemplele de la exercițiul 3 (fără a folosi eauto).

5. (8 puncte) Demonstrați proprietățile: progress (5 puncte), type preservation (1 punct) și type soundness (2 puncte) pentru limbajul de expresii.

Coq Reference Manual: https://coq.inria.fr/distrib/current/refman/