Mathematical Software – ICMS 2020
7th International Conference, Braunschweig, Germany, July 13–16, 2020, Proceedings
Page
%P
-
Chapter and Conference Paper
Compositional Reversible Computation
Reversible computing is motivated by both pragmatic and foundational considerations arising from a variety of disciplines. We take a particular path through the development of reversible computation, emphasizing
-
Article
State of the Practice for Lattice Boltzmann Method Software
We analyze the state of software development practice for Lattice Boltzmann solvers by quantitatively and qualitatively measuring and comparing 24 software packages for 10 software qualities (installability, c...
-
Article
Open AccessBig Math and the One-Brain Barrier: The Tetrapod Model of Mathematical Knowledge
-
Book and Conference Proceedings
-
Chapter and Conference Paper
Leveraging the Information Contained in Theory Presentations
A theorem prover without an extensive library is much less useful to its potential users. Algebra, the study of algebraic structures, is a core component of such libraries. Algebraic theories also are themselv...
-
Chapter and Conference Paper
Fractional Types
In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a matching de-allocation. Seco...
-
Chapter and Conference Paper
Towards Specifying Symbolic Computation
Many interesting and useful symbolic computation algorithms manipulate mathematical expressions in mathematically meaningful ways
-
Article
Seismology software: state of the practice
We analyzed the state of practice for software development in the seismology domain by comparing 30 software packages on four aspects: product, implementation, design, and process. We found room for improvemen...
-
Chapter and Conference Paper
Biform Theories: Project Description
A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for specifying and reasoning about algorithms that man...
-
Chapter and Conference Paper
A Library of Reversible Circuit Transformations (Work in Progress)
Isomorphisms between finite types directly correspond to combinational, reversible, logical gates. Categorically they are morphisms in special classes of (bi-)monoidal categories. The coherence conditions for ...
-
Chapter and Conference Paper
HOL Light QE
We are interested in algorithms that manipulate mathematical expressions in mathematically meaningful ways. Expressions are syntactic, but most logics do not allow one to discuss syntax.
-
Chapter and Conference Paper
Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study
A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for formalizing algorithms that manipulate mathematica...
-
Chapter and Conference Paper
Probabilistic Inference by Program Transformation in Hakaru (System Description)
We present Hakaru, a new probabilistic programming system that allows composable reuse of distributions, queries, and inference algorithms, all expressed in a single language of measures. The system implements...
-
Chapter and Conference Paper
Computing with Semirings and Weak Rig Groupoids
The original formulation of the Curry–Howard correspondence relates propositional logic to the simply-typed \(\lambda \) ...
-
Chapter and Conference Paper
Simplifying Probabilistic Programs Using Computer Algebra
We transform probabilistic programs to run more efficiently and read more easily, by composing three semantics-preserving transformations: (1) apply the denotational semantics; (2) improve the resulting integr...
-
Book and Conference Proceedings
Intelligent Computer Mathematics
International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings.
-
Chapter and Conference Paper
Realms: A Structure for Consolidating Knowledge about Mathematical Theories
Since there are different ways of axiomatizing and develo** a mathematical theory, knowledge about a such a theory may reside in many places and in many forms within a library of formalized mathematics. We i...
-
Book and Conference Proceedings
Intelligent Computer Mathematics
MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings
-
Book and Conference Proceedings
Intelligent Computer Mathematics
11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings
-
Chapter and Conference Paper
Theory Presentation Combinators
We motivate and give semantics to theory presentation combinators as the foundational building blocks for a scalable library of theories. The key observation is that the category of contexts and fibered categorie...
