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

Anders Schack-Nielsen, Carsten Schürmann

    Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

    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 .
    Original languageEnglish
    Book seriesLecture Notes in Computer Science
    Pages (from-to)320-326
    ISSN0302-9743
    DOIs
    Publication statusPublished - 2008
    EventInternational Joint Conference, IJCAR 2008 - Sydney, Australia
    Duration: 12 Aug 200815 Aug 2008
    Conference number: 4

    Conference

    ConferenceInternational Joint Conference, IJCAR 2008
    Number4
    Country/TerritoryAustralia
    CitySydney
    Period12/08/200815/08/2008

    Keywords

    • Concurrent Logical Framework
    • Celf
    • Linear Types
    • Concurrency
    • Judgments-as-Types

    Cite this