Mode checking in HAL

Maria Jose Garcia De La Banda; Peter J Stuckey; Warwick Harvey; Kim Marriott

doi:10.1007/3-540-44957-4_85

Mode checking in HAL

Maria Jose Garcia De La Banda, Peter J Stuckey, Warwick Harvey, Kim Marriott

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

6 Citations (Scopus)

Abstract

Recent constraint logic programming (CLP) languages, such as HAL and Mercury, require type, mode and determinism declarations for predicates. This information allows the generation of efficient target code and the detection of many errors at compile-time. However, mode checking in such languages is difficult since the compiler is required to appropriately re-order literals in the predicate’s definition for each predicate mode declaration. The task is further complicated by the need to handle complex instantiations which interact with type declarations, higher order functions and predicates, and automatic initialization of solver variables. Here we give the first formal treatment of mode checking in strongly typed CLP languages which require reordering of clause body literals during mode checking. We also sketch the mode checking algorithms used in the HAL compiler.

Original language	English
Title of host publication	Computational Logic – CL 2000
Subtitle of host publication	First International Conference London, UK, July 24-28, 2000 Proceedings
Editors	John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luís Moniz Pereira, Yehoshua Sagiv, Peter J. Stuckey
Place of Publication	Berlin Germany
Publisher	Springer
Pages	1270-1284
Number of pages	15
ISBN (Print)	3540677976
DOIs	https://doi.org/10.1007/3-540-44957-4_85
Publication status	Published - 2000
Event	International Conference on Computational Logic 2000 - London, United Kingdom Duration: 24 Jul 2000 → 28 Jul 2000 Conference number: 1st https://link-springer-com.ezproxy.lib.monash.edu.au/book/10.1007/3-540-44957-4 (Proceedings)

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1861
ISSN (Print)	0302-9743

Conference

Conference	International Conference on Computational Logic 2000
Abbreviated title	CL 2000
Country/Territory	United Kingdom
City	London
Period	24/07/00 → 28/07/00
Internet address	https://link-springer-com.ezproxy.lib.monash.edu.au/book/10.1007/3-540-44957-4 (Proceedings)

Access to Document

10.1007/3-540-44957-4_85

Cite this

Garcia De La Banda, M. J., Stuckey, P. J., Harvey, W., & Marriott, K. (2000). Mode checking in HAL. In J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, & P. J. Stuckey (Eds.), Computational Logic – CL 2000: First International Conference London, UK, July 24-28, 2000 Proceedings (pp. 1270-1284). (Lecture Notes in Computer Science; Vol. 1861). Springer. https://doi.org/10.1007/3-540-44957-4_85

Garcia De La Banda, Maria Jose ; Stuckey, Peter J ; Harvey, Warwick et al. / Mode checking in HAL. Computational Logic – CL 2000: First International Conference London, UK, July 24-28, 2000 Proceedings. editor / John Lloyd ; Veronica Dahl ; Ulrich Furbach ; Manfred Kerber ; Kung-Kiu Lau ; Catuscia Palamidessi ; Luís Moniz Pereira ; Yehoshua Sagiv ; Peter J. Stuckey. Berlin Germany : Springer, 2000. pp. 1270-1284 (Lecture Notes in Computer Science).

@inproceedings{4453e0004a7f4b64b6c2d070aa4d0e3f,

title = "Mode checking in HAL",

abstract = "Recent constraint logic programming (CLP) languages, such as HAL and Mercury, require type, mode and determinism declarations for predicates. This information allows the generation of efficient target code and the detection of many errors at compile-time. However, mode checking in such languages is difficult since the compiler is required to appropriately re-order literals in the predicate{\textquoteright}s definition for each predicate mode declaration. The task is further complicated by the need to handle complex instantiations which interact with type declarations, higher order functions and predicates, and automatic initialization of solver variables. Here we give the first formal treatment of mode checking in strongly typed CLP languages which require reordering of clause body literals during mode checking. We also sketch the mode checking algorithms used in the HAL compiler.",

author = "{Garcia De La Banda}, {Maria Jose} and Stuckey, {Peter J} and Warwick Harvey and Kim Marriott",

year = "2000",

doi = "10.1007/3-540-44957-4_85",

language = "English",

isbn = "3540677976",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "1270--1284",

editor = "John Lloyd and Veronica Dahl and Ulrich Furbach and Manfred Kerber and Kung-Kiu Lau and Catuscia Palamidessi and Pereira, {Lu{\'i}s Moniz} and Yehoshua Sagiv and Stuckey, {Peter J.}",

booktitle = "Computational Logic – CL 2000",

note = "International Conference on Computational Logic 2000, CL 2000 ; Conference date: 24-07-2000 Through 28-07-2000",

url = "https://link-springer-com.ezproxy.lib.monash.edu.au/book/10.1007/3-540-44957-4",

}

Garcia De La Banda, MJ , Stuckey, PJ, Harvey, W & Marriott, K 2000, Mode checking in HAL. in J Lloyd, V Dahl, U Furbach, M Kerber, K-K Lau, C Palamidessi, LM Pereira, Y Sagiv & PJ Stuckey (eds), Computational Logic – CL 2000: First International Conference London, UK, July 24-28, 2000 Proceedings. Lecture Notes in Computer Science, vol. 1861, Springer, Berlin Germany, pp. 1270-1284, International Conference on Computational Logic 2000, London, United Kingdom, 24/07/00. https://doi.org/10.1007/3-540-44957-4_85

Mode checking in HAL. / Garcia De La Banda, Maria Jose ; Stuckey, Peter J; Harvey, Warwick et al.
Computational Logic – CL 2000: First International Conference London, UK, July 24-28, 2000 Proceedings. ed. / John Lloyd; Veronica Dahl; Ulrich Furbach; Manfred Kerber; Kung-Kiu Lau; Catuscia Palamidessi; Luís Moniz Pereira; Yehoshua Sagiv; Peter J. Stuckey. Berlin Germany: Springer, 2000. p. 1270-1284 (Lecture Notes in Computer Science; Vol. 1861).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Mode checking in HAL

AU - Garcia De La Banda, Maria Jose

AU - Stuckey, Peter J

AU - Harvey, Warwick

AU - Marriott, Kim

N1 - Conference code: 1st

PY - 2000

Y1 - 2000

N2 - Recent constraint logic programming (CLP) languages, such as HAL and Mercury, require type, mode and determinism declarations for predicates. This information allows the generation of efficient target code and the detection of many errors at compile-time. However, mode checking in such languages is difficult since the compiler is required to appropriately re-order literals in the predicate’s definition for each predicate mode declaration. The task is further complicated by the need to handle complex instantiations which interact with type declarations, higher order functions and predicates, and automatic initialization of solver variables. Here we give the first formal treatment of mode checking in strongly typed CLP languages which require reordering of clause body literals during mode checking. We also sketch the mode checking algorithms used in the HAL compiler.

AB - Recent constraint logic programming (CLP) languages, such as HAL and Mercury, require type, mode and determinism declarations for predicates. This information allows the generation of efficient target code and the detection of many errors at compile-time. However, mode checking in such languages is difficult since the compiler is required to appropriately re-order literals in the predicate’s definition for each predicate mode declaration. The task is further complicated by the need to handle complex instantiations which interact with type declarations, higher order functions and predicates, and automatic initialization of solver variables. Here we give the first formal treatment of mode checking in strongly typed CLP languages which require reordering of clause body literals during mode checking. We also sketch the mode checking algorithms used in the HAL compiler.

U2 - 10.1007/3-540-44957-4_85

DO - 10.1007/3-540-44957-4_85

M3 - Conference Paper

SN - 3540677976

T3 - Lecture Notes in Computer Science

SP - 1270

EP - 1284

BT - Computational Logic – CL 2000

A2 - Lloyd, John

A2 - Dahl, Veronica

A2 - Furbach, Ulrich

A2 - Kerber, Manfred

A2 - Lau, Kung-Kiu

A2 - Palamidessi, Catuscia

A2 - Pereira, Luís Moniz

A2 - Sagiv, Yehoshua

A2 - Stuckey, Peter J.

PB - Springer

CY - Berlin Germany

T2 - International Conference on Computational Logic 2000

Y2 - 24 July 2000 through 28 July 2000

ER -

Garcia De La Banda MJ , Stuckey PJ, Harvey W, Marriott K. Mode checking in HAL. In Lloyd J, Dahl V, Furbach U, Kerber M, Lau KK, Palamidessi C, Pereira LM, Sagiv Y, Stuckey PJ, editors, Computational Logic – CL 2000: First International Conference London, UK, July 24-28, 2000 Proceedings. Berlin Germany: Springer. 2000. p. 1270-1284. (Lecture Notes in Computer Science). doi: 10.1007/3-540-44957-4_85