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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	Electronic Notes in Theoretical Computer Science : Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008
Redaktører	A. Abel, C. Urban
Vol/bind	228
Forlag	Pergamon Press
Publikationsdato	2009
Sider	113-120
DOI	https://doi.org/10.1016/j.entcs.2008.12.120
Status	Udgivet - 2009
Begivenhed	International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with - Pittsburgh, Pennsylvania, USA Varighed: 23 jun. 2008 → 23 jun. 2008

Konference

Konference	International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with
Land/Område	USA
By	Pittsburgh, Pennsylvania
Periode	23/06/2008 → 23/06/2008

Emneord

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

Adgang til dokumentet

10.1016/j.entcs.2008.12.120

Citationsformater

Schürmann, C., & Poswolsky, A. (2009). System Description: Delphin - A Functional Programming Language for Deductive Systems. I A. Abel, & C. Urban (red.), Electronic Notes in Theoretical Computer Science: Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008 (Bind 228, s. 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. i A Abel & C Urban (red), Electronic Notes in Theoretical Computer Science: Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008. bind 228, Pergamon Press, s. 113-120, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08) Affiliated with, Pittsburgh, Pennsylvania, USA, 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. red. / A. Abel; C. Urban. Bind 228 Pergamon Press, 2009. s. 113-120.

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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. I Abel A, Urban C, red., Electronic Notes in Theoretical Computer Science: Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008. Bind 228. Pergamon Press. 2009. s. 113-120 doi: 10.1016/j.entcs.2008.12.120