We introduce a system of monadic affine sized types, which substantially generalizes usual sized types and allows in this way to capture probabilistic higher-order programs that terminate almost surely. Going beyond plain, strong normalization without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. The way typable programs are proved to be almost surely terminating is based on reducibility but requires a substantial adaptation of the technique.

Lago U.D., Grellois C. (2019). Probabilistic termination by monadic affine sized typing. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 41(2), 1-65 [10.1145/3293605].

Probabilistic termination by monadic affine sized typing

Lago U. D.;
2019

Abstract

We introduce a system of monadic affine sized types, which substantially generalizes usual sized types and allows in this way to capture probabilistic higher-order programs that terminate almost surely. Going beyond plain, strong normalization without losing soundness turns out to be a hard task, which cannot be accomplished without a richer, quantitative notion of types, but also without imposing some affinity constraints. The proposed type system is powerful enough to type classic examples of probabilistically terminating programs such as random walks. The way typable programs are proved to be almost surely terminating is based on reducibility but requires a substantial adaptation of the technique.
2019
Lago U.D., Grellois C. (2019). Probabilistic termination by monadic affine sized typing. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 41(2), 1-65 [10.1145/3293605].
Lago U.D.; Grellois C.
File in questo prodotto:
File Dimensione Formato  
ACMTrans2019.pdf

accesso aperto

Tipo: Postprint
Licenza: Licenza per accesso libero gratuito
Dimensione 841.45 kB
Formato Adobe PDF
841.45 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/732572
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 15
  • ???jsp.display-item.citation.isi??? 11
social impact