Curry and Howard meet Borel

DOI10.1145/3531130.3533361MaRDI QIDQ6649480zbMATH OpenFDO

Authors Melissa Antonelli, Ugo Dal Lago, Paolo Pistone

Publication date 6 December 2024

Full work available at URL https://doi.org/10.1145/3531130.3533361

zbMATH Keywords

counting logicCurry-Howard correspondenceintersection typesprobabilistic computationtermination

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• Towards probabilistic reasoning in type theory -- the intersection type case
• A Type Theory for Probabilistic \lambda –calculus
• Lambda calculus and probabilistic computation
• A probabilistic semantics for the pure \(\lambda\)-calculus
• Statistical properties of simple types

Cites work

• A core quantitative coeffect calculus
• A decisive characterization of BPP
• A double category theoretic analysis of graded linear exponential comonads
• A logic for reasoning about time and reliability
• A modal analysis of staged computation
• A theory of effects and resources: adjunction models and polarised calculi
• An analysis of first-order logics of probability
• Bounded Linear Logic, Revisited
• Bounded linear logic: A modular approach to polynomial-time computability
• Bounded Linear Types in a Resource Semiring
• Combinatory logic. With two sections by William Craig.
• Computational types from a logical perspective
• Decomposing probabilistic lambda calculi
• Games against nature
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 2046116 (Why is no real title available?)
• scientific article; zbMATH DE number 2134919 (Why is no real title available?)
• scientific article; zbMATH DE number 1848312 (Why is no real title available?)
• scientific article; zbMATH DE number 2090077 (Why is no real title available?)
• Lectures on the Curry-Howard isomorphism
• Linear logic propositions as session types
• Markov logic networks
• Measure quantifier in monadic second order logic
• Modal intersection types, two-level languages, and staged synthesis
• Monadic Second Order Logic with Measure and Category Quantifiers
• On counting propositional logic and Wagner's hierarchy
• On measure quantifiers in first-order arithmetic
• On the termination problem for probabilistic higher-order recursive programs
• Parametric effect monads and semantics of effect systems
• Probabilistic call by push value
• Probabilistic coherence spaces are fully abstract for probabilistic PCF
• Probabilistic logic
• Probabilistic logic revisited
• Probabilistic logics based on Riesz spaces
• Probabilistic quantifiers and games
• Probabilistic termination by monadic affine sized typing
• Propositions as sessions
• Reasoning about knowledge and probability
• Reasoning with time and chance
• Semantics of probabilistic programs
• Some observations on the connection between counting and recursion
• The complexity of combinatorial problems with succinct input representation
• The geometry of parallelism: classical, probabilistic, and quantum effects
• The measure quantifier

Cited in

(1)

• Simple types for probabilistic termination

This page was built for publication: Curry and Howard meet Borel

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6649480)