Celf – A Logical Framework for Deductive and Concurrent Systems (System Description) Export

@incollection{citeulike:5916291, abstract = {CLF (Concurrent LF) [CPWW02a] is a logical framework for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, security protocol analysis, process algebras, and logics. Celf is an implementation of the CLF type theory that extends the LF type theory by linear types to support representation of state and a monad to support representation of concurrency. It relies on the judgments-as-types methodology for specification and the interpretation of CLF signatures as concurrent logic programs [LPPW05] for experimentation. Celf is written in Standard ML and compiles with MLton, MLKit, and SML/NJ. The source code and a collection of examples are available from http://www.twelf.org/\~{}celf .}, author = {Schack-Nielsen, Anders and Sch\"{u}rmann, Carsten}, citeulike-article-id = {5916291}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-540-71070-7_28}, citeulike-linkout-1 = {http://www.springerlink.com/content/m552397v5401836p}, doi = {10.1007/978-3-540-71070-7_28}, journal = {Automated Reasoning}, keywords = {clf, concurrency, linear-logic, logical-frameworks, modal-logic}, pages = {320--326}, posted-at = {2009-10-09 15:13:39}, priority = {0}, title = {Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)}, url = {http://dx.doi.org/10.1007/978-3-540-71070-7_28}, year = {2008} }

TY - CHAP ID - citeulike:5916291 L3 - citeulike-article-id:5916291 N2 - CLF (Concurrent LF) [CPWW02a] is a logical framework for specifying and implementing deductive and concurrent systems from areas, such as programming language theory, security protocol analysis, process algebras, and logics. Celf is an implementation of the CLF type theory that extends the LF type theory by linear types to support representation of state and a monad to support representation of concurrency. It relies on the judgments-as-types methodology for specification and the interpretation of CLF signatures as concurrent logic programs [LPPW05] for experimentation. Celf is written in Standard ML and compiles with MLton, MLKit, and SML/NJ. The source code and a collection of examples are available from http://www.twelf.org/~celf . JF - Automated Reasoning EP - 326 TI - Celf – A Logical Framework for Deductive and Concurrent Systems (System Description) SP - 320 KW - clf KW - concurrency KW - linear-logic KW - logical-frameworks KW - modal-logic AU - Schack-Nielsen, Anders AU - Schürmann, Carsten PY - 2008/// UR - http://dx.doi.org/10.1007/978-3-540-71070-7_28 ER -