Výsledky vyhledávání - "Aloïs Brunel"

Akademický článek

Church => Scott = Ptime: an application of resource sensitive realizability

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 23, Iss Proc. DICE 2010, Pp 31-46 (2010)

We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed by a standard non-linear type `Church,' while the Scott encodings (pure

Externí odkaz: https://doaj.org/article/457c438561d740f4a9317a5f3e641939

Zobrazit plný text záznamu

Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation

Autor: Damiano Mazza, Aloïs Brunel, Michele Pagani

Publikováno v: Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2020

Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably m

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b0166fd027d6bf2e21010b388dfa7223
https://hal.archives-ouvertes.fr/hal-02400927

Zobrazit plný text záznamu

Realizability models for a linear dependent PCF

Autor: Aloïs Brunel, Marco Gaboardi

Publikováno v: Theoretical Computer Science. 585:55-70

Recently, Dal Lago and Gaboardi have proposed a type system, named d l PCF as a framework for implicit computational complexity. d l PCF is a non-standard type system for PCF programs which is relatively complete with respect to quantitative properti

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::5da6f50398c802ce503d1001f057b179
https://doi.org/10.1016/j.tcs.2015.03.005

Zobrazit plný text záznamu

Quantitative classical realizability

Autor: Aloïs Brunel

Publikováno v: Information and Computation. 241:62-95

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 u

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ca4c35449650fbf714f603843248313b
https://doi.org/10.1016/j.ic.2014.10.007

Zobrazit plný text záznamu

A Core Quantitative Coeffect Calculus

Autor: Marco Gaboardi, Aloïs Brunel, Steve Zdancewic, Damiano Mazza

Publikováno v: Programming Languages and Systems ISBN: 9783642548321
ESOP

Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. Its resource-awareness arises from the distinction between linear, single-use data and non-

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::4f074d9d2ab43940dc889afad277428b
https://doi.org/10.1007/978-3-642-54833-8_19

Zobrazit plný text záznamu

Indexed realizability for bounded-time programming with references and type fixpoints

Autor: Antoine Madet, Aloïs Brunel

Publikováno v: Programming Languages and Systems-10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-December 13, 2012. Proceedings
APLAS
Programming Languages and Systems ISBN: 9783642351815

International audience; The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging to a certain complexity class. We here present

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ec52c3206f294769a9da1c321db76373
https://hal.archives-ouvertes.fr/hal-00735584

Zobrazit plný text záznamu

Orthogonality and Boolean Algebras for Deduction Modulo

Autor: Aloïs Brunel, Olivier Hermant, Clément Houtmann

Publikováno v: Lecture Notes in Computer Science ISBN: 9783642216909
TLCA

Originating from automated theorem proving, deduction modulo removes computational arguments from proofs by interleaving rewriting with the deduction process. From a proof-theoretic point of view, deduction modulo defines a generic notion of cut that

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::6c8e79fef8a9bb2ec7971ca0f70c342b
https://doi.org/10.1007/978-3-642-21691-6_9

Zobrazit plný text záznamu

Akademický článek

The Tortoise and the Hare Algorithm for Finite Lists, Compositionally.

Autor: DANVY, OLIVIER¹ danvy@acm.org

Publikováno v: ACM Transactions on Programming Languages & Systems. Mar2023, Vol. 45 Issue 1, p1-35. 35p.

Zobrazit plný text záznamu

Akademický článek

VERIFYING AN EFFECT-HANDLER-BASED DEFINE-BY-RUN REVERSE-MODE AD LIBRARY.

Autor: DE VILHENA, PAULO EMÍLIO, POTTIER, FRANÇOIS

Publikováno v: Logical Methods in Computer Science (LMCS); 2023, Vol. 19 Issue 4, p1-51, 51p

Zobrazit plný text záznamu

Implicit Complexity in Concurrent Lambda-Calculi

Autor: Madet, Antoine

Publikováno v: Programming Languages [cs.PL]. Université Paris-Diderot-Paris VII, 2012. English

Controlling the resource consumption of programs is crucial: besides performance reasons, it has many applications in the field of computer security where e.g. mobile or embedded systems dispose of limited amounts of resources. In this thesis, we dev

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=od______2592::44790fb77bf02b4b55a83dccb932db25
https://tel.archives-ouvertes.fr/tel-00794977/document

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání