Seminari del Dipartimento

Logica e Informatica Teorica

Nul besoin de système pour raisonner, il suffit d’utiliser des tests. Jusqu’à une date récente, je pensais que cette approche d’usine achoppait sur des problèmes de finitude. Mais si l’on considère des tests suffisants (pas nécessaires donc), les batteries de tests peuvent rester finies. L’opposition traditionnelle entre Curry et Church se retrouve sous la forme usage/usine. L’usage (BHK) définit les signifiants logiques implicitement : le type comme comportement. L’usine (Herbrand) définit les signifiants logiques explicitement : le type comme critère de correction.

Ces deux approches sont reliées par un résultat d’adéquation, élimination des coupures si l’on veut : les tests suffisent à garantir l’usage. La trinité réaliste axiomatique syntaxe/sémantique/méta est ainsi remplacée par une trinité déréaliste usine/usage/adéquation.

(Nota: il seminario sarà tenuto in lingua francese)

Per partecipare al seminario:
chiedere il link all’indirizzo email vitomichele.abrusci@uniroma3.it  
o cliccare sul seguente link Teams Meeting
org: PEDICINI Marco