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

Carsten Schürmann; Adam Poswolsky

doi:10.1016/j.entcs.2008.12.120

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

Computer Science

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-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 language	English
Title of host publication	Electronic Notes in Theoretical Computer Science : Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008
Editors	A. Abel, C. Urban
Volume	228
Publisher	Pergamon Press
Publication date	2009
Pages	113-120
DOIs	https://doi.org/10.1016/j.entcs.2008.12.120
Publication status	Published - 2009
Event	International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with - Pittsburgh, Pennsylvania, United States Duration: 23 Jun 2008 → 23 Jun 2008

Conference

Conference	International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with
Country/Territory	United States
City	Pittsburgh, Pennsylvania
Period	23/06/2008 → 23/06/2008

Keywords

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

Access to Document

10.1016/j.entcs.2008.12.120

Cite this

Schürmann, C., & Poswolsky, A. (2009). System Description: Delphin - A Functional Programming Language for Deductive Systems. In A. Abel, & C. Urban (Eds.), Electronic Notes in Theoretical Computer Science: Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008 (Vol. 228, pp. 113-120). Pergamon Press. https://doi.org/10.1016/j.entcs.2008.12.120

@inproceedings{54e44c30e2ec11dda259000ea68e967b,

title = "System Description:: Delphin - A Functional Programming Language for Deductive Systems",

abstract = "Delphin is a functional programming language [Adam Poswolsky and Carsten Sch{\"u}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.",

keywords = "Functional Programming, Dependent Types, Higher-Order Encodings, Decidable Type Checking, Pattern Matching, Functional Programming, Dependent Types, Higher-Order Encodings, Decidable Type Checking, Pattern Matching",

author = "Carsten Sch{\"u}rmann and Adam Poswolsky",

year = "2009",

doi = "10.1016/j.entcs.2008.12.120",

language = "English",

volume = "228",

pages = "113--120",

editor = "A. Abel and C. Urban",

booktitle = "Electronic Notes in Theoretical Computer Science",

publisher = "Pergamon Press",

note = "International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with ; Conference date: 23-06-2008 Through 23-06-2008",

}

Schürmann, C & Poswolsky, A 2009, System Description: Delphin - A Functional Programming Language for Deductive Systems. in A Abel & C Urban (eds), Electronic Notes in Theoretical Computer Science: Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008. vol. 228, Pergamon Press, pp. 113-120, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with, Pittsburgh, Pennsylvania, United States, 23/06/2008. https://doi.org/10.1016/j.entcs.2008.12.120

System Description: Delphin - A Functional Programming Language for Deductive Systems. / Schürmann, Carsten; Poswolsky, Adam.
Electronic Notes in Theoretical Computer Science: Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008. ed. / A. Abel; C. Urban. Vol. 228 Pergamon Press, 2009. p. 113-120.

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - System Description:

T2 - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with

AU - Schürmann, Carsten

AU - Poswolsky, Adam

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - Functional Programming

KW - Dependent Types

KW - Higher-Order Encodings

KW - Decidable Type Checking

KW - Pattern Matching

KW - Functional Programming

KW - Dependent Types

KW - Higher-Order Encodings

KW - Decidable Type Checking

KW - Pattern Matching

U2 - 10.1016/j.entcs.2008.12.120

DO - 10.1016/j.entcs.2008.12.120

M3 - Article in proceedings

VL - 228

SP - 113

EP - 120

BT - Electronic Notes in Theoretical Computer Science

A2 - Abel, A.

A2 - Urban, C.

PB - Pergamon Press

Y2 - 23 June 2008 through 23 June 2008

ER -

Schürmann C, Poswolsky A. System Description: Delphin - A Functional Programming Language for Deductive Systems. In Abel A, Urban C, editors, Electronic Notes in Theoretical Computer Science: Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008. Vol. 228. Pergamon Press. 2009. p. 113-120 doi: 10.1016/j.entcs.2008.12.120