<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>

COPY SCRIPT

For further information contact us at helpdesk@openaire.eu

A Formalisation of a Turing-Complete Choreographic Language in Coq

Name: A Formalisation of a Turing-Complete Choreographic Language in Coq
Keywords: Infectious Diseases, Sociology, Genetics, Plant Biology, Endpoint Projection, Choreographic Programming, Biochemistry, Partial Recursive Functions, Turing Completeness, Biological Sciences not elsewhere classified

integration_instructionsResearch softwarekeyboard_double_arrow_right Software 29 Jan 2021Publisher:Zenodo

Authors: Cruz-Filipe, Luís; Montesi, Fabrizio; Peressotti, Marco;

doi: 10.5281/zenodo.4548709 , 10.5281/zenodo.4479102 , 10.5281/zenodo.4479101

A Formalisation of a Turing-Complete Choreographic Language in Coq

- Summary
- Subjects
- Related research
  (1)
- Metrics

Abstract

A formalisation in Coq of: a choreographic programming language (CC.v) Kleene's theory of partial recursive functions (Kleene.v) an encoding of Kleene's RPFs as choreographies and the proof of its correctness (Implementation.v) a calculus of stateful processes (SP.v) a certified compiler for the choreographic language to the process calculus (EPP.v, Merge.v, Pruning.v)

Related Organizations

University of Southern Denmark
Denmark

Keywords

Infectious Diseases, Sociology, Genetics, Plant Biology, Endpoint Projection, Choreographic Programming, Biochemistry, Partial Recursive Functions, Turing Completeness, Biological Sciences not elsewhere classified

1 Research products, page 1 of 1

A Formal Theory of Choreographic Programming in Coq
2022IsAmongTopNSimilarDocuments

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	1
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average