Extracting nondeterministic concurrent programs
- Submitting institution
-
Swansea University / Prifysgol Abertawe
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 28974
- Type
- E - Conference contribution
- DOI
-
10.4230/LIPIcs.CSL.2016.26
- Title of conference / published proceedings
- 25th EACSL Annual Conference on Computer Science Logic (CSL 2016).
- First page
- 26:1
- Volume
- 62
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- December
- Year of publication
- 2016
- URL
-
https://drops.dagstuhl.de/opus/volltexte/2016/6566/pdf/LIPIcs-CSL-2016-26.pdf
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The formal specification and modelling of concurrent and non-deterministic computation is hugely important but notoriously difficult. Current research in this area concentrates on properties of computation such as equivalence and refinement of processes, or models for different forms of choice operators. We go a big step further by connecting non-determinism and concurrency to a logical system that can express high-level specifications of programs that are directly relevant to the user. The result is a system where computational problems can be abstractly specified and their possibly non-deterministic and concurrent solutions automatically extracted and synthesied from proofs.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -