Dependently Typed Languages in Statix

Autor: Brouwer, Jonathan, Cockx, J.G.H., Zwaan, A.S., Lammel, Ralf, Mosses, Peter D., Steimann, Friedrich

Publikováno v: Eelco Visser Commemorative Symposium, EVCS 2023

Static type systems can greatly enhance the quality of programs, but implementing a type checker that is both expressive and user-friendly is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e584d30e3b0dcdbd191965519ad63d14
http://resolver.tudelft.nl/uuid:cfe5ad16-3938-4ab5-b438-a8220a15f068

Embedding the refinement calculus in Coq

Autor: João Alpuim, Wouter Swierstra

Publikováno v: Science of Computer Programming. 164:37-48

The refinement calculus and type theory are both frameworks that support the specification and verification of programs. This paper presents an embedding of the refinement calculus in the interactive theorem prover Coq, clarifying the relation betwee

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::3392cf21337a11f83d5f031d03b5f3e6
https://doi.org/10.1016/j.scico.2017.04.003

Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)

Autor: Timany, Amin, Sozeau, Matthieu

Publikováno v: [Research Report] RR-9105, KU Leuven, Belgium; Inria Paris. 2017, pp.30
[Research Report] RR-9105, KU Leuven, Belgium; Inria Paris. 2017, pp.32

Version 2 fixes some typos from version 1.Version 3 fixes a typo in a typing rule from version 2.; In order to avoid well-know paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a co

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::212d0a4ac5bed1ab72c4e9c0015422b0
https://hal.inria.fr/hal-01615123

J-Calc: A Typed Lambda Calculus for Intuitionistic Justification Logic

Autor: Giuseppe Primiero, Konstantinos Pouliasis

Publikováno v: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

In this paper we offer a system J-Calc that can be regarded as a typed λ-calculus for the {→,⊥} fragment of Intuitionistic Justification Logic. We offer different interpretations of J-Calc, in particular, as a two phase proof system in which we

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::dc374257d6bf13913b76269dbbecc363

Encoding Proofs in Dedukti: the case of Coq proofs

Autor: Assaf, Ali, Dowek, Gilles, Jouannaud, Jean-Pierre, Liu, Jiaxiang

Publikováno v: Proc. HaTT
Proceedings Hammers for Type Theories
Proceedings Hammers for Type Theories, Jul 2016, Coimbra, Portugal

International audience; A main ambition of the Inria project Dedukti is to serve as a common language for representing and type checking proof objects originating from other proof systems. Encoding these proof objects makes heavy use of the rewriting

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::b51f323c3421bd4824a1abce02baaa6d
https://hal.inria.fr/hal-01330980/document