System Description: Delphin - A Functional Programming Language for Deductive Systems

Carsten Schürmann, Adam Poswolsky

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    Abstract

    Delphin is a functional programming language [Adam Poswolsky and Carsten Schürmann. Practical programming with higher-order encodings and dependent types. In European Symposium on Programming (ESOP), 2008] utilizing dependent higher-order datatypes. Delphin's two-level type-system cleanly separates data from computation, allowing for decidable type checking. The data level is LF [Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143-184, January 1993], which allows for the specification of deductive systems following the judgments-as-types methodology. The computation level facilitates the manipulation of such encodings by providing facilities for pattern matching, recursion, and the dynamic creation of new parameters (which can be thought of as scoped constants). Delphin's documentation and examples are available online at http://delphin.logosphere.org.
    Original languageEnglish
    Title of host publicationElectronic Notes in Theoretical Computer Science : Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008
    EditorsA. Abel, C. Urban
    Volume228
    PublisherPergamon Press
    Publication date2009
    Pages113-120
    DOIs
    Publication statusPublished - 2009
    EventInternational Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with - Pittsburgh, Pennsylvania, United States
    Duration: 23 Jun 200823 Jun 2008

    Conference

    ConferenceInternational Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with
    Country/TerritoryUnited States
    CityPittsburgh, Pennsylvania
    Period23/06/200823/06/2008

    Keywords

    • Functional Programming
    • Dependent Types
    • Higher-Order Encodings
    • Decidable Type Checking
    • Pattern Matching

    Cite this