Outputs (5)

Modular and efficient top-down parsing for ambiguous left-recursive grammars (2007)
Presentation / Conference Contribution
Frost, R., Hafiz, R., & Callaghan, P. (2007, June). Modular and efficient top-down parsing for ambiguous left-recursive grammars. Presented at 10th International Conference on Parsing Technology : IWPT'07, Prague

In functional and logic programming, parsers can be built as modular executable specifications of grammars, using parser combinators and definite clause grammars respectively. These techniques are based on top-down backtracking search. Commonly used... Read More about Modular and efficient top-down parsing for ambiguous left-recursive grammars.

LFTOP : an LF-based approach to domain-specific reasoning (2005)
Journal Article
Pang, J., Callaghan, P., & Luo, Z. (2005). LFTOP : an LF-based approach to domain-specific reasoning. Journal of Computer Science and Technology, 20(4), 526-535. https://doi.org/10.1007/s11390-005-0526-y

A new approach to domain-specific reasoning is presented that is based on a type-theoretic logical framework (LF) but does not require the user to be an expert in type theory. The concepts of the domain and its related reasoning systems are formalize... Read More about LFTOP : an LF-based approach to domain-specific reasoning.

Types for proofs and programs : international workshop, TYPES 2000, Durham UK, December 8-12, 2000 (2002)
Book
Callaghan, P., Luo, Z., McKinna, J., & Pollack, R. (Eds.). (2002). Types for proofs and programs : international workshop, TYPES 2000, Durham UK, December 8-12, 2000. Springer Verlag. https://doi.org/10.1007/3-540-45842-5

Object languages in a type-theoretic meta-framework (2001)
Presentation / Conference Contribution
Callaghan, P., Luo, Z., & Pang, J. (2001, June). Object languages in a type-theoretic meta-framework. Presented at Proof Transformation and Presentation and Proof Complexities Workshop : PTP'01., Siena, Italy

This paper concerns techniques for providing a convenient syntax for object languages implemented via a type-theoretic Logical Framework, and reports on work in progress. We first motivate the need for a type-theoretic logical framework. Firstly, we... Read More about Object languages in a type-theoretic meta-framework.

An implementation of LF with coercive subtyping & universes (2001)
Journal Article
Callaghan, P., & Luo, Z. (2001). An implementation of LF with coercive subtyping & universes. Journal of Automated Reasoning, 27(1), 3-27. https://doi.org/10.1023/a%3A1010648911114

We present Plastic, an implementation of LF with Coercive Subtyping, and focus on its implementation of Universes. LF is a variant of Martin-Löf''s logical framework, with explicitly typed -abstractions. We outline the system of LF with its extension... Read More about An implementation of LF with coercive subtyping & universes.