Formal Methods

3 articles

• La Correspondance de Curry-Howard : lien entre programmes et preuves5 min de lecture

  La correspondance de Curry-Howard, parfois appelée isomorphisme de Curry-Howard, établit une équivalence profonde entre deux domaines apparemment distincts : la logique formelle et la théorie des type...

• Propositions as types : l'unification de Wadler4 min de lecture

  Philip Wadler, dans sa conférence et son article « Propositions as Types », offre une méditation historique et philosophique sur la correspondance de Curry-Howard.

• Refinement Types et Dependent Types : vers des types qui prouvent4 min de lecture

  Au-delà du typage classique, certains systèmes permettent d'encoder des propriétés plus fines. Le compilateur devient alors un assistant de preuve, et permet de forcer des invariants métiers encore pl...