A type system for Continuation Calculus

Autor: Geuvers, H., Geraedts, W., Geron, B., Stegeren, J. van, Oliva, P.
Přispěvatelé: Oliva, P., Formal System Analysis
Jazyk: angličtina
Rok vydání: 2014
Předmět:
Zdroj: Electronic Proceedings in Theoretical Computer Science, Vol 164, Iss Proc. CL&C 2014, Pp 1-17 (2014)
Oliva, P. (ed.), Proceedings Fifth International Workshop on Classical Logic and Computation Vienna, Austria, July 13, 2014, pp. 1-17
Fifth International Workshop on Classical Logic and Computation (Vienna, Austria, July 13, 2014), 1-17
STARTPAGE=1;ENDPAGE=17;TITLE=Fifth International Workshop on Classical Logic and Computation (Vienna, Austria, July 13, 2014)
Electronic Proceedings in Theoretical Computer Science ; 164, 1-17. [S.l.] : EPTCS
STARTPAGE=1;ENDPAGE=17;TITLE=Electronic Proceedings in Theoretical Computer Science ; 164
ISSN: 2075-2180
Popis: Continuation Calculus (CC), introduced by Geron and Geuvers, is a simple foundational model for functional computation. It is closely related to lambda calculus and term rewriting, but it has no variable binding and no pattern matching. It is Turing complete and evaluation is deterministic. Notions like "call-by-value" and "call-by-name" computation are available by choosing appropriate function definitions: e.g. there is a call-by-value and a call-by-name addition function. In the present paper we extend CC with types, to be able to define data types in a canonical way, and functions over these data types, defined by iteration. Data type definitions follow the so-called "Scott encoding" of data, as opposed to the more familiar "Church encoding". The iteration scheme comes in two flavors: a call-by-value and a call-by-name iteration scheme. The call-by-value variant is a double negation variant of call-by-name iteration. The double negation translation allows to move between call-by-name and call-by-value.
Comment: In Proceedings CL&C 2014, arXiv:1409.2593
Databáze: OpenAIRE
Externí odkaz: