<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

CPP21 Artifact - Machine-Checked Semantic Session Typing

Name: CPP21 Artifact - Machine-Checked Semantic Session Typing
Creator: Hinrichsen, jonas Kastberg

integration_instructionsResearch softwarekeyboard_double_arrow_right Software 15 Dec 2020 English Publisher:Zenodo

Authors: Hinrichsen, jonas Kastberg;

doi: 10.5281/zenodo.4322751 , 10.5281/zenodo.4322752

CPP21 Artifact - Machine-Checked Semantic Session Typing

- Summary
- Subjects
- Metrics

Abstract

This is the artifact corresponding to the CPP21 paper "Machine-Checked Semantic Session Typing" by Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson. The latest version of the artifact can be obtained online at https://gitlab.mpi-sws.org/iris/actris. The semantic session type system is a part of the Actris repository and thus the artifact includes both. The artifact is provided in two forms: - As a virtual machine, including all dependencies. You can import the `cpp_vm.ova` into VirtualBox ("File -- Import Appliance"). After starting the machine, additional instructions can be found in the `README` file on the Desktop. The VM supports both Emacs and CoqIDE - As a tarball of source file, including the Iris dependency repositories. You can extract `cpp_coq.tar.gz` anywhere, and then follow the instructions in the `README.md` file. The artifact has been tested with VirtualBox version 6.1, which can be downloaded for all major platforms from [virtualbox.org](https://www.virtualbox.org/wiki/Downloads) Login information Username: actris Password: password Admin password: admin

Related Organizations

IT University of Copenhagen
Denmark

Keywords

Message passing, concurrency, session types, separation logic, semantic typing, Iris, Coq

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).	0
	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

Usage byUsageCounts

visibility	views	43
download	downloads	8

43
views
8
downloads
Powered by

Found an issue? Give us feedback

visibility

download

Average