Operational Semantics of Resolution and Productivity in Horn Clause Logic
- Submitting institution
-
Heriot-Watt University
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 16546112
- Type
- D - Journal article
- DOI
-
10.1007/s00165-016-0403-1
- Title of journal
- Formal Aspects of Computing
- Article number
- -
- First page
- 453
- Volume
- 29
- Issue
- 3
- ISSN
- 0934-5043
- Open access status
- Compliant
- Month of publication
- November
- Year of publication
- 2016
- 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
-
1
- Research group(s)
-
-
- Citation count
- 6
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Output of EPSRC grants EP/K031864/1-2, the journal paper presents constructive type-theoretic semantics for different kinds of resolution that appeared in the literature. The results have significance for the growing number of applications of automated proving in type inference in programming languages. This paper laid groundwork for related FLOPS'16, LOPSTR'16, ICLP'18, ESOP'19 papers by Komendantskaya on type inference in Haskell and dependent types. The latter two papers form PhD thesis (2020) of Komendantskaya's student Farka. The results were recognized by invited talks at Oxford, Birmingham, Bath, Dagstuhl, Cambridge, Midlands Graduate School, Programming Languages&Compilers'16.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
