Zobrazeno 1 - 4
of 4
pro vyhledávání: '"Andrés Sicard-Ramírez"'
Publikováno v:
Logic Journal of the IGPL. 30:777-806
A version of intuitionistic type theory is extended with opposite types, allowing a different formalization of negation and obtaining a paraconsistent type theory ($\textsf{PTT} $). The rules for opposite types in $\textsf{PTT} $ are based on the rul
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b5e94e17df1ec36ab549a3e5078bee4a
https://doi.org/10.1093/jigpal/jzab022
https://doi.org/10.1093/jigpal/jzab022
A paraconsistent type theory (an extension of a fragment of intuitionistic type theory by adding opposite types) is here extended by adding co-function types. It is shown that, in the extended paraconsistent type system, the opposite type constructor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::aa9645a9ceaeb3f8f78448eebe57c5c2
http://arxiv.org/abs/2204.03882
http://arxiv.org/abs/2204.03882
Publikováno v:
Foundations of Software Science and Computational Structures ISBN: 9783642287282
FoSSaCS
FoSSaCS
We propose a new approach to the computer-assisted verification of functional programs. We work in first order theories of functional programs which are obtained by extending Aczel's first order theory of combinatory formal arithmetic with positive i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::67ac590ba521dfc44884069abc7473c2
https://doi.org/10.1007/978-3-642-28729-9_7
https://doi.org/10.1007/978-3-642-28729-9_7
Publikováno v:
PLPV
We propose a new way to reason about general recursive functional programs in the dependently typed programming language Agda, which is based on Martin-Lof's intuitionistic type theory. We show how to embed an external programming logic, Aczel's Logi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::caa7f3d3a9a29bf48ce625b94147d95f
https://doi.org/10.1145/1481848.1481857
https://doi.org/10.1145/1481848.1481857