Three examples of compositional type systems are briefly illustrated. The question is whether people working on programming languages and people workingon formal verification feel the need to identify a suite of code reuse/modularization mechanisms for synergically addressing- fine-grained code reuse- coarse-grained code reuse- spatial/temporal code evolution while being suitable for compositional analysis. Perhaps, being suitable for compositional typing could be a preliminary requisite for such a suite of mechanisms. A reformulation of the question: is it feasible for this research community to agree on a list of recommendations / guidelines / principles to be taken into account when designing a new language (or evolving an existing one) in order to facilitate formal verification?

Three cases of composition and a question

DAMIANI, Ferruccio
2013-01-01

Abstract

Three examples of compositional type systems are briefly illustrated. The question is whether people working on programming languages and people workingon formal verification feel the need to identify a suite of code reuse/modularization mechanisms for synergically addressing- fine-grained code reuse- coarse-grained code reuse- spatial/temporal code evolution while being suitable for compositional analysis. Perhaps, being suitable for compositional typing could be a preliminary requisite for such a suite of mechanisms. A reformulation of the question: is it feasible for this research community to agree on a list of recommendations / guidelines / principles to be taken into account when designing a new language (or evolving an existing one) in order to facilitate formal verification?
2013
Divide and Conquer: the Quest for Compositional Design and Analysis (Dagstuhl Seminar 12511)
Dagstuhl, Germany
December 17-21, 2012
Divide and Conquer: the Quest for Compositional Design and Analysis
2
12
72
72
http://drops.dagstuhl.de/opus/volltexte/2013/3995/
http://www.dagstuhl.de/mat/Files/12/12511/12511.DamianiFerruccio.Slides.pdf
http://www.dagstuhl.de/no_cache/en/program/calendar/semhp/?semnr=12511
Algorithm; Design; Language; Theory; Verification
Ferruccio Damiani
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/2318/139518
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact