Quantitative classical realizability
| Autor: | Aloïs Brunel |
|---|---|
| Rok vydání: | 2015 |
| Předmět: |
FOS: Computer and information sciences
Soundness Computer Science - Logic in Computer Science Forcing (recursion theory) Multiplicative function Linear logic Logic in Computer Science (cs.LO) Computer Science Applications Theoretical Computer Science Algebra Computable function Computational Theory and Mathematics Computer Science::Logic in Computer Science Bounded function Realizability Time complexity Information Systems Mathematics |
| Zdroj: | Information and Computation. 241:62-95 |
| ISSN: | 0890-5401 |
| DOI: | 10.1016/j.ic.2014.10.007 |
| Popis: | Introduced by Dal Lago and Hofmann, quantitative realizability is a technique used to define models for logics based on Multiplicative Linear Logic. A particularity is that functions are interpreted as bounded time computable functions. It has been used to give new and uniform proofs of soundness of several type systems with respect to certain time complexity classes. We propose a reformulation of their ideas in the setting of Krivine's classical realizability. The framework obtained generalizes Dal Lago and Hofmann's realizability, and reveals deep connections between quantitative realizability and a linear variant of Cohen's forcing. Comment: Revised version |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect