The true concurrency of Herbrand's theorem
- Submitting institution
-
University of Strathclyde
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 107580199
- Type
- E - Conference contribution
- DOI
-
10.4230/LIPIcs.CSL.2018.5
- Title of conference / published proceedings
- 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
- First page
- 5:1
- Volume
- 119
- Issue
- -
- ISSN
- 1868-8969
- Open access status
- Compliant
- Month of publication
- August
- Year of publication
- 2018
- URL
-
-
- 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
-
3
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The paper provides a new semantics to classical proofs as winning concurrent strategies and through this provides a compositional proof of Herbrand's classical theorem via a semantic model; previous proofs were via proof normalisation so not compositional. Since this paper, issues, formerly of a purely proof-theoretic nature (e.g. Miller's expansion trees) have become refined and analysable in the new semantics of classical proof. The work formed the cornerstone of Alcolei's PhD thesis at ENS Lyon and led to Winskel's invited talk at the major meeting of French researchers Journees Nationales 2018 du GDR Informatique Mathematique, Palaiseau.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -