Nov. 18th, 2018

xacid: (Default)
https://www.sciencedirect.com/science/article/pii/S016800721200084X

Towards a canonical classical natural deduction system
JoséEspírito Santo

This paper studies a new classical natural deduction system, presented as a typed calculus. It is designed to be isomorphic to Curien and Herbelinʼs-calculus, both at the level of proofs and reduction, and the isomorphism is based on the correct correspondence between cut (resp. left-introduction) in sequent calculus, and substitution (resp. elimination) in natural deduction. It is a combination of Parigotʼs λμ-calculus with the idea of “coercion calculus” due to Cervesato and Pfenning, accommodating let-expressions in a surprising way: they expand Parigotʼs syntactic class of named terms.
xacid: (Default)
https://www.cs.indiana.edu/~sabry/papers/rational.pdf

The Two Dualities of Computation:
Negative and Fractional Types
Roshan P. James
Indiana University
rpjames@indiana.edu
Amr Sabry
Indiana University
sabry@indiana.edu

Every functional programmer knows about sum and product types,
a+b and a×b respectively. Negative and fractional types,
a−b and a/b respectively, are much less known and their computational in-
terpretation is unfamiliar and often complicated. We show that in a
programming model in which information is preserved (such as the
model introduced in our recent paper on Information Effects), these
types have particularly natural computational interpretations. Intu-
itively, values of negative types are values that flow “backwards” to
satisfy demands and values of fractional types are values that im-
pose constraints on their context. The combination of these negative
and fractional types enables greater flexibility in programming by
breaking global invariants into local ones that can be autonomously
satisfied by a subcomputation. Theoretically, these types give rise to
two function spaces and to two notions of continuations, suggesting
that the previously observed duality of computation conflated two
orthogonal notions: an additive duality that corresponds to backtracking
and a multiplicative duality that corresponds to constraint propagation

Profile

xacid: (Default)
xacid

April 2021

S M T W T F S
    123
45678910
11121314151617
18192021222324
252627282930 

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 11th, 2025 04:49 am
Powered by Dreamwidth Studios