|
| |
Delphin
 |
Adam Poswolsky. Functional
Programming with Logical Frameworks: The Delphin Project, Ph.D.
Dissertation, CreateSpace, 2008. ISBN 978-1440474927 (PDF,
Amazon) .
|
|
Adam Poswolsky
and Carsten Schürmann. System
Description: Delphin – A Functional Programming Language for Deductive
Systems. In
International Workshop on Logical Frameworks and Metalanguages: Theory
and Practice (LFMTP ’08), Electronic Notes in Theoretical Computer
Science (ENTCS), pages 135–141, Pittsburgh, PA, June 2008.
Elsevier. (PDF)
|
|
Adam Poswolsky
and Carsten Schürmann. Practical
Programming with Higher-Order Encodings and Dependent Types.
In
European Symposium on Programming
(ESOP 2008), pages 93–107,
Budapest,
Hungary,
2008. ISBN 978-3-540-78738-9.
 |
Full Version (PDF) |
|
Extended Technical Report,
YALEU/DCS/TR-1375 (PDF)
|
|
Earlier Design of Delphin
|
Adam Poswolsky.
A Temporal-Logic Approach to
Functional Calculi for Dependent Types and Higher-Order Encodings,
YALEU/DCS/TR-1364, 2006.
|
∇/Elphin Specific
Related:
|
Miller and Tiu, A Proof Theory for Generic Judgments: An
extended abstract. (PDF) |
Related: Selected Publications regarding the Meta Logical Framework
Twelf
| [S01a]
Carsten Schürmann. Recursion for Higher-Order Encodings. Proceedings
of Computer Science Logic (CSL 2001), Paris, France. LNCS 2142, pp 585-599,
2001 |
| [S00b]
Carsten Schürmann. Automating the Meta-Theory of Deductive Systems.
PhD thesis, Carnegie-Mellon University, 2000. CMU- CS-00-146 |
| [S00a]
Carsten Schürmann. A Meta Logical Framework Based on Realizability. Workshop
on Logical Frameworks and Meta-Languages (LFM 2000), Santa Barbara,
California, June 2000. |
| [PS99]
Frank Pfenning and Carsten Schürmann. System description: Twelf --- a
meta-logical framework for deductive systems. In H. Ganzinger, editor,
Proceedings of the 16th International Conference on Automated Deduction
(CADE-16), pages 202--206, Trento, Italy, July 1999. Springer-Verlag LNAI
1632. |
| [SP98]
Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple
meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors,
Proceedings of the 15th International Conference on Automated Deduction
(CADE-15), pages 286--300, Lindau, Germany, July 1998. Springer-Verlag
LNCS 1421. |
|
