We provide a construction that, given a big-step semantics describing finite computations and their observations, extends it to include infinite computations as well. The basic idea is that the finite behavior uniquely determines the infinite behavior once observations and their composition operators are fixed. Technically, the construction relies on the framework of inference systems with corules. The effectiveness and scope of the approach are illustrated by several examples. The correctness is formally justified by proving that, starting from a big-step semantics equivalent to a reference small-step semantics, this equivalence is preserved by the construction.

A big step from finite to infinite computations

Ancona D.;Dagnino F.;Zucca E.
2020-01-01

Abstract

We provide a construction that, given a big-step semantics describing finite computations and their observations, extends it to include infinite computations as well. The basic idea is that the finite behavior uniquely determines the infinite behavior once observations and their composition operators are fixed. Technically, the construction relies on the framework of inference systems with corules. The effectiveness and scope of the approach are illustrated by several examples. The correctness is formally justified by proving that, starting from a big-step semantics equivalent to a reference small-step semantics, this equivalence is preserved by the construction.
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Descrizione: Articolo su rivista
Tipologia: Documento in Post-print
Dimensione 324.11 kB
Formato Adobe PDF
324.11 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/11567/1035233
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact