|
| |
Delphin Current
 |
Adam Poswolsky and Carsten Schürmann. Delphin: A
Functional Programming Language with Higher-Order Encodings and
Dependent Types. (Submitted) (PDF).
|
Delphin Earlier
|
Adam Poswolsky. A Temporal-Logic Approach to
Functional Calculi for Dependent Types and Higher-Order Encodings.
|
|
Adam Poswolsky and Carsten Schürmann. A Temporal-Logic
Approach to Programming with Dependent Types and Higher-Order Encodings.
YALEU/DCS/TR-1355 (PDF) (Twelf
Code) |
∇/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. |
|
