• 学术搜索
  • 科研智能体
    • Research Labs
    • AI 阅读
    • AI 文库
    • 深度研究
    • 学者亮点
  • 学术资源
    • AI2000
    • 期刊/会议
    • 学者库
    • 学术API
      MCP&Skill
    • 溯源树
    • 数据集
  • 知识沉淀
    • 学术空间
订阅小程序
旧版功能
aminer vip
开通会员低至0.73元/天
一次搞定AI科研
立即登录
  • English
  • 联系方式
    Mathematical Foundations of Programming Semantics

    Mathematical Foundations of Programming Semantics

    Conference

    年发文量

    研究主题

    论文(618)

    排序
    1Polynomial Universes and Dependent Types.
    C. B. Aberlé, David I. Spivak
    2025
    引用
    AI阅读
    加入学术空间
    2A Fresh Look at Bivariate Binomial Distributions
    Bart Jacobs

    Binomial distributions capture the probabilities of `heads' outcomes when a (biased) coin is tossed multiple times. The coin may be identified with a distribution on the two-element set 0,1, where the 1 outcome corresponds to `head'. One can also toss two separate coins, with different biases, in parallel and record the outcomes. This paper investigates a slightly different `bivariate' binomial distribution, where the two coins are dependent (also called: entangled, or entwined): the two-coin is a distribution on the product 0,1 x 0,1. This bivariate binomial exists in the literature, with complicated formulations. Here we use the language of category theory to give a new succint formulation. This paper investigates, also in categorically inspired form, basic properties of these bivariate distributions, including their mean, variance and covariance, and their behaviour under convolution and under updating, in Laplace's rule of succession. Furthermore, it is shown how Expectation Maximisation works for these bivariate binomials, so that mixtures of bivariate binomials can be recognised in data. This paper concentrates on the bivariate case, but the binomial distributions may be generalised to the multivariate case, with multiple dimensions, in a straightforward manner.

    2025
    引用
    AI阅读
    加入学术空间
    3Compositional Inference for Bayesian Networks and Causality
    Bart Jacobs, Márk Széles,Dario Stein

    Inference is a fundamental reasoning technique in probability theory. When applied to a large joint distribution, it involves updating with evidence (conditioning) in one or more components (variables) and computing the outcome in other components. When the joint distribution is represented by a Bayesian network, the network structure may be exploited to proceed in a compositional manner -- with great benefits. However, the main challenge is that updating involves (re)normalisation, making it an operation that interacts badly with other operations. String diagrams are becoming popular as a graphical technique for probabilistic (and quantum) reasoning. Conditioning has appeared in string diagrams, in terms of a disintegration, using bent wires and shaded (or dashed) normalisation boxes. It has become clear that such normalisation boxes do satisfy certain compositional rules. This paper takes a decisive step in this development by adding a removal rule to the formalism, for the deletion of shaded boxes. Via this removal rule one can get rid of shaded boxes and terminate an inference argument. This paper illustrates via many (graphical) examples how the resulting compositional inference technique can be used for Bayesian networks, causal reasoning and counterfactuals. 21 pages, 2 figures. To be published in MFPS 2025 proceedings

    2025引用:2
    引用
    AI阅读
    加入学术空间
    4Modular Abstract Syntax Trees (MAST): Substitution Tensors with Second-Class Sorts
    Marcelo P. Fiore,Ohad Kammar,Georg Moser,Sam Staton

    We adapt Fiore, Plotkin, and Turi's treatment of abstract syntax with binding, substitution, and holes to account for languages with second-class sorts. These situations include programming calculi such as the Call-by-Value lambda-calculus (CBV) and Levy's Call-by-Push-Value (CBPV). Prohibiting second-class sorts from appearing in variable contexts changes the characterisation of the abstract syntax from monoids in monoidal categories to actions in actegories. We reproduce much of the development through bicategorical arguments. We apply the resulting theory by proving substitution lemmata for varieties of CBV.

    2025
    引用
    AI阅读
    加入学术空间
    5Compact Quantitative Theories of Convex Algebras
    Matteo Mio

    We introduce the concept of compact quantitative equational theory. A quantitative equational theory is defined to be compact if all its consequences are derivable by means of finite proofs. We prove that the theory of interpolative barycentric (also known as convex) quantitative algebras of Mardare et. al. is compact. This serves as a paradigmatic example, used to obtain other compact quantitative equational theories of convex algebras, each axiomatizing some distance on finitely supported probability distributions.

    2025引用:4
    引用
    AI阅读
    加入学术空间
    立即登录,查看全部 618 篇论文

    高被引作者

    作者引用发文
    John C. Reynolds5891
    Luca Viganò4231
    John Mitchell3663
    Jan J.M.M. Rutten3334
    Karel Hrbacek2931
    Pierre America2691
    John Power23811
    Frank Pfenning2365
    Patrick Cousot2152
    Anupam Datta1993

    高产作者

    作者引用发文
    Stephen Brookes18515
    John Power23811
    Bart Jacobs14411
    Robin Cockett659
    Achim Jung1699
    Alexandra Silva608
    Prakash Panangaden718
    Sam Staton757
    Rasmus Ejlers Møgelberg896
    Michael Mislove676

    相关期刊

    Types for Proofs and Programs
    Conference on Algebra and Coalgebra in Computer Science
    Annual Conference for Computer Science Logic
    Developments in Computational Models
    Formal Structures for Computation and Deduction
    Foundations of Software Science and Computation Structure
    International Conference on Applications of Declarative Programming and Knowledge Management
    Logical and Semantic Frameworks with Applications
    Mathematics of Program Construction
    International Conference on Relational and Algebraic Methods in Computer Science