Our vision is to use mathematics to understand the nature of computation, and to turn that understanding into the next generation of programming languages.

We see the mathematical foundations of computation and programming as inextricably linked. We study one so as to develop the other. This reflects the symbiotic relationship between mathematics, programming, and the design of programming languages — any attempt to sever this connection will diminish each component.

A formal type of proof most frequently encountered in elementary geometry courses in which known or derived statements are written in the left column, and the reason that each statement is known or valid is written next to it in the right column. The proof then proceeds from the known facts to the theorem to be demonstrated. […] However, this form of proof is virtually never used by practicing mathematicians because its confining and verbose format render it of very limited utility to any but the most simple of theorems.

Hmm, maybe this is why people don’t like Lean LOL.

Today we’re excited to announce the first alpha release of CatColab 0.2: Wren. CatColab is software for making models of the world together.

Novel developments in theoretical and applied category theory enable users to design database schemas, create casual flows, and construct manifold PDEs using a single fluid syntax, and migrate between these different modes using functors.

In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects.

Coinduction is the mathematical dual to structural induction. Coinductively defined data types are known as codata and are typically infinite data structures, such as streams.

As a definition or specification, coinduction describes how an object may be “observed”, “broken down” or “destructed” into simpler objects. As a proof technique, it may be used to show that an equation is satisfied by all possible implementations of such a specification.