Iowa Type Theory Commute

Latest Episodes:

More on FP and concise code Dec 12, 2019

Show notes

Discussion of datatypes for tree-like data structures in functional languages. Usefulness of these for processing structured linguistic artifacts, where the structure is represented by the tree structure.

Functional Programming and Concise Code: Type Inference Dec 12, 2019

Show notes

Start of discussion of some of technology and culture that lead to more concise code in functional programming languages. Type inference to avoid writing types for local and input variables. Some basics of static and dynamic typing.

Introduction to Functional Programming Dec 11, 2019

Show notes

Introduction to the basic idea of functional programming. Three kinds are discussed: functional programming with mutable state, pure functional programming (where there is no implicit state), and strong functional programming (which is pure functional programming where every function is statically required to terminate).

Software Engineering Considerations for Formal Methods Dec 01, 2019

Show notes

Discussion of some practicalities of applying formal methods to software. Ideally we are seeking techniques that can be applied with increasing effort to yield increasingly strong results. Also, introduction to functional programming.

Power of Computer-Checked Proofs for Software Nov 30, 2019

Show notes

Continuing pessimistic discussion about the purpose of formal methods for Computer Science. But then counter arguments about the value of absolutely correct software.

Technical reasons for lack of adoption of computer-checked proofs Nov 28, 2019

Show notes

Discussion of a technical reason for lack of adoption of computer-checked proofs for mathematics, namely the level of detail in the proof. Proof assistants require too much detail in proofs to allow mathematicians to carry over their elegant art of expressing just the right amount of information to convey the idea of the proof to a mathematically competent reader. For Computer Science, a problem of adoption is that proofs are computationally useless (generally).

Why Computer-Checked Proofs are Not Used More in Mathematics Nov 27, 2019

Show notes

Some discussion of why computer-checked proofs have not been adopted more in mathematics. The psychology of telling mathematicians their time-honored method of investigation is inadequate and they need computer-checked proofs. Computer-checked proofs and certainty.

Computer-Checked Proofs in American Research Nov 26, 2019

Show notes

Some pockets of interest in computer-checked proofs in the US in the 1980s and 1990s. Several important research projects and initiatives in the US in the late 1990s and early 2000s that helped raise awareness in the US of computer-checked proofs: proof-carrying code, the POPLmark challenge.

Computer-checked proofs about software Nov 23, 2019

Show notes

Computer-checked proofs can ensure properties of software. Discussion of several aspects of this idea.

More on Computer-Checked Proofs Nov 22, 2019

Show notes

Further discussion of computer-checked proofs, including the example of the proof by Hales and his collaborators of the Kepler Conjecture. Automath also mentioned. DAO hack on Ethereum and the interest in cryptocurrency community in computer-checked proofs.

Our TOPPODCAST Picks

Follow Us

Stay Connected

Related Podcasts

Links

Stay Connected

Our TOPPODCAST Picks

Follow Us

Stay Connected

Iowa Type Theory Commute

Related Podcasts

1

2

3

4

5

6