Skip to Main content Skip to Navigation
Conference papers

Towards an implementation of a logical framework based on intersection and union types

Abstract : We present an ongoing implementation of a dependent-type the- ory (∆-framework) based on the Edinburgh Logical Framework LF, extended with Proof-functional logical connectives such as in- tersection, union, and strong (or minimal relevant) implication. Their combination opens up new possibilities of formal reasoning on proof-theoretic semantics. We provide some examples in the extended type theory and we outline a type checker. The theory of the system is under investigation. Once validated in vitro, the proof-functional type theory could be successfully plugged into existing truth-functional proof-systems.
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-01534035
Contributor : Luigi Liquori <>
Submitted on : Wednesday, June 7, 2017 - 9:36:29 AM
Last modification on : Friday, October 20, 2017 - 10:06:01 AM
Document(s) archivé(s) le : Friday, September 8, 2017 - 12:11:01 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01534035, version 1

Citation

Claude Stolze, Luigi Liquori. Towards an implementation of a logical framework based on intersection and union types. International Workshop on Logical Frameworks and Meta-languages, Sep 2017, Oxford, United Kingdom. ⟨hal-01534035v1⟩

Share

Metrics

Record views

90

Files downloads

30