Juntar-se

Revistas

Actas de conferências

ElPub

[Electronic Publishing]

ElPub

Electronic Publishing

A conferência ElPub, realizada anualmente entre 1997 e 2020, apresenta os resultados da investigação sobre vários aspectos da publicação digital, envolvendo uma comunidade internacional diversificada de todas as disciplinas das ciências e humanidades.

A última conferência ElPub foi realizada em 2020; os textos das conferências de 2018, 2019 e 2020 ainda estão disponíveis no sítio Web.

  • Tipo de suporte: digital
  • Periodicidade: anual
  • Estado da coleção: 2018-2020
  • Data de disponibilização online na Episciences: 2018
  • Idiomas da publicação: inglês
Ver o sítio web

Últimos artigos

Actas de conferências
Informática e matemática aplicada

ENTICS

[Electronic Notes in Theoretical Informatics and Computer Science]

ENTICS

Electronic Notes in Theoretical Informatics and Computer Science

A ENTICS, Electronic Notes in Theoretical Informatics and Computer Science, criada em 2022, publica, gradualmente em inglês, atas de conferências e de workshops de informática teórica.

  • Diretor de publicação: Bruno Sportisse
  • Redator responsável: Michael Mislove
  • Tipo de suporte: digital
  • Periodicidade: gradual
  • Ano de criação: 2022
  • Data de disponibilização online na Episciences: 2023
  • eISSN: 2969-2431
  • Disciplinas: informática teórica
  • Idiomas da publicação: inglês
  • Processo de avaliação: estudo cego
  • Licence CC BY 4.0
  • Editor: Inria
    • Endereço postal: Domaine de Voluceau Rocquencourt – B.P. 105 78153 Le Chesnay Cedex
    • País: França
  • Contacto: entics AT episciences.org
Ver o sítio web

Últimos artigos

Implicit automata in {\lambda}-calculi III: affine planar string-to-string functions

We prove a characterization of first-order string-to-string transduction via $\lambda$-terms typed in non-commutative affine logic that compute with Church encoding, extending the analogous known characterization of star-free languages. We show that every first-order transduction can be computed by a $\lambda$-term using a known Krohn-Rhodes-style decomposition lemma. The converse direction is given by compiling $\lambda$-terms into two-way reversible planar transducers. The soundness of this translation involves showing that the transition functions of those transducers live in a monoidal closed category of diagrams in which we can interpret purely affine $\lambda$-terms. One challenge is that the unit of the tensor of the category in question is not a terminal object. As a result, our interpretation does not identify $\beta$-equivalent terms, but it does turn $\beta$-reductions into inequalities in a poset-enrichment of the category of diagrams.
Pradic, Cécilia
December 11, 2024
Ler o artigo

Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory

We study a cost-aware programming language for higher-order recursion dubbed $\textbf{PCF}_\mathsf{cost}$ in the setting of synthetic domain theory (SDT). Our main contribution relates the denotational cost semantics of $\textbf{PCF}_\mathsf{cost}$ to its computational cost semantics, a new kind of dynamic semantics for program execution that serves as a mathematically natural alternative to operational semantics in SDT. In particular we prove an internal, cost-sensitive version of Plotkin's computational adequacy theorem, giving a precise correspondence between the denotational and computational semantics for complete programs at base type. The constructions and proofs of this paper take place in the internal dependent type theory of an SDT topos extended by a phase distinction in the sense of Sterling and Harper. By controlling the interpretation of cost structure via the phase distinction in the denotational semantics, we show that $\textbf{PCF}_\mathsf{cost}$ programs also evince a noninterference property of cost and behavior. We verify the axioms of the type theory by means of a model construction based on relative sheaf models of SDT.
Niu, Yue
December 11, 2024
Ler o artigo