We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expres- sive type system for the probabilistic event λ-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. In this context, proofs (respectively, types) do not guarantee that validity (respectively, termination) holds, but reveal the underlying proba- bility. We finally show how to obtain a system precisely capturing the probabilistic behavior of λ-terms, by endowing the type system with an intersection operator.

Curry and Howard Meet Borel

Melissa Antonelli;Ugo Dal Lago;Paolo Pistone
2022

Abstract

We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expres- sive type system for the probabilistic event λ-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. In this context, proofs (respectively, types) do not guarantee that validity (respectively, termination) holds, but reveal the underlying proba- bility. We finally show how to obtain a system precisely capturing the probabilistic behavior of λ-terms, by endowing the type system with an intersection operator.
2022
In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '22)
1
13
Melissa Antonelli; Ugo Dal Lago; Paolo Pistone
File in questo prodotto:
File Dimensione Formato  
lics2022a.pdf

accesso aperto

Tipo: Versione (PDF) editoriale
Licenza: Licenza per Accesso Aperto. Altra tipologia di licenza compatibile con Open Access
Dimensione 897.58 kB
Formato Adobe PDF
897.58 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/904337
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact