Algebra of programming

Foundations of Algebraic Specification and Formal Software Development

This book provides foundations for software specification and formal software development from the perspective of work on algebraic specification, concentrating on developing basic concepts and studying their fundamental properties. These foundations are built on a solid mathematical basis, using elements of universal algebra, category theory and logic, and this mathematical toolbox provides a convenient language for precisely formulating the concepts involved in software specification and development. Once formally defined, these notions become subject to mathematical investigation, and this interplay between mathematics and software engineering yields results that are mathematically interesting, conceptually revealing, and practically useful. The theory presented by the authors has its origins in work on algebraic specifications that started in the early 1970s, and their treatment is comprehensive. This book contains five kinds of material: the requisite mathematicalfoundations; traditional algebraic specifications; elements of the theory of institutions; formal specification and development; and proof methods. While the book is self-contained, mathematical maturity and familiarity with the problems of software engineering is required; and in the examples that directly relate to programming, the authors assume acquaintance with the concepts of functional programming. The book will be of value to researchers and advanced graduate students in the areas of programming and theoretical computer science.

Programming Language Foundations in Agda – Table of Contents

This book is an introduction to programming language theory using the proof assistant Agda.

EbookFoundation/free-programming-books

:books: Freely available programming books

Category theory for computing science

Category theory for computing science by Michael Barr, 1990, Prentice Hall edition, in English

Computational category theory

Computational category theory by D. E. Rydeheard, 1988, Prentice Hall edition, in English

A theory of type polymorphism in programming

The aim of this work is largely a practical one. A widely employed style of programming, particularly in structure-processing languages which impose n…

GATlab: Modeling and Programming with Generalized Algebraic Theories

Categories and categorical structures are increasingly recognized as useful abstractions for modeling in science and engineering. To uniformly implement category-theoretic mathematical models in software, we introduce GATlab, a domain-specific language for algebraic specification embedded in a technical programming language. GATlab is based on generalized algebraic theories (GATs), a logical system extending algebraic theories with dependent types so as to encompass category theory. Using GATlab, the programmer can specify generalized algebraic theories and their models, including both free models, based on symbolic expressions, and computational models, defined by arbitrary code in the host language. Moreover, the programmer can define maps between theories and use them to declaratively migrate models of one theory to models of another. In short, GATlab aims to provide a unified environment for both computer algebra and software interface design with generalized algebraic theories. In this paper, we describe the design, implementation, and applications of GATlab.

Functional programming with bananas, lenses, envelopes and barbed wire

We develop a calculus for lazy functional programming based on recursion operators associated with data type definitions. For these operators we derive various algebraic laws that are useful in deriving and manipulating programs. We shall show that all example functions in Bird and Wadler's “Introduction to Functional Programming” can be expressed using these operators.

Coconut Programming Language

Simple, elegant, Pythonic functional programming.

Elements of Programming

After ten years in print, our publisher decided against further printings and reverted the rights to us. Elements of Programming is now available in two forms: a free PDF and a no-markup paperback.

Reading

Carl Kolon's favorite articles about programming.

Packrat parsing: | Proceedings of the seventh ACM SIGPLAN international conference on Functional programming

For decades we have been using Chomsky's generative system of grammars, particularly context-free grammars (CFGs) and regular expressions (REs), to express the syntax of programming languages and protocols. The power of generative grammars to express ...

OCaml Programming: Correct + Efficient + Beautiful — OCaml Programming: Correct + Efficient + Beautiful

A textbook on functional programming and data structures in OCaml, with an emphasis on semantics and software engineering. This book is the textbook for CS 3110 Data Structures and Functional Programming at Cornell University. A past title of this book was “Functional Programming in OCaml”.