2026-07-22T01:29:21Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9936 2024-03-06T10:45:09Z ddc:004 open_access

The Delta-Framework Honsell, Furio Liquori, Luigi Stolze, Claude Scagnetto, Ivan Logic of programs type theory lambda-calculus We introduce the Delta-framework, LF_Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong proof-functional connectives take into account the shape of logical proofs, thus reflecting polymorphic features of proofs in formulae. This is in contrast to classical or intuitionistic connectives where the meaning of a compound formula depends only on the truth value or the provability of its subformulae. Our framework encompasses a wide range of type disciplines. Moreover, since relevant implication permits to express subtyping, LF_Delta subsumes also Pfenning's refinement types. We discuss the design decisions which have led us to the formulation of LF_Delta, study its metatheory, and provide various examples of applications. Our strong proof-functional type theory can be plugged in existing common proof assistants. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Furio Honsell and Luigi Liquori and Claude Stolze and Ivan Scagnetto 2018 Is Part Of LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2018.37 urn:nbn:de:0030-drops-99367 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.37 eng https://creativecommons.org/licenses/by/3.0/legalcode