|
Interaction nets
|
|
0
|
1
|
April 2, 2025
|
|
Practical Alloy - a guide to formal software design
|
|
0
|
1
|
February 20, 2025
|
|
Anatomy of a formal proof
|
|
0
|
1
|
January 27, 2025
|
|
Streams, Calculation Proofs, and Dafny
|
|
0
|
1
|
August 8, 2024
|
|
Granule - linear functional language with graded modal types
|
|
0
|
2
|
July 4, 2024
|
|
A Graph-Based Higher-Order Intermediate Representation
|
|
0
|
3
|
March 24, 2024
|
|
SAT/SMT by example
|
|
0
|
2
|
March 24, 2024
|
|
Liquid Types vs. Floyd-Hoare Logic
|
|
0
|
2
|
March 24, 2024
|
|
Cost-aware type theory
|
|
0
|
2
|
March 24, 2024
|
|
Cubical Type Theory
|
|
0
|
2
|
March 24, 2024
|
|
Refinement types - a tutorial
|
|
0
|
3
|
March 24, 2024
|
|
Modular Type Classes
|
|
0
|
2
|
March 24, 2024
|
|
Software Foundations (books on logic and semantics of programming languages)
|
|
0
|
3
|
March 24, 2024
|
|
Java and Scala’s Type Systems are Unsound
|
|
0
|
2
|
March 24, 2024
|
|
A catalogue of optimizing transformations
|
|
0
|
2
|
March 23, 2024
|
|
δ-Complete Decision Procedures for Satisfiability over the Reals
|
|
0
|
3
|
March 23, 2024
|
|
An argument against call/cc
|
|
0
|
2
|
March 23, 2024
|
|
Bartosz Milewski's Programming Cafe
|
|
0
|
2
|
March 23, 2024
|
|
Corecursion and coinduction
|
|
0
|
2
|
March 23, 2024
|
|
Awesome Recursion Schemes
|
|
0
|
3
|
March 23, 2024
|
|
Hoare's hints on programming language design
|
|
0
|
2
|
March 23, 2024
|
|
Set-Theoretic Types for Polymorphic Variants
|
|
0
|
3
|
March 23, 2024
|
|
Type inference with subtyping
|
|
0
|
2
|
March 23, 2024
|
|
Proof that "algebraic datatypes" are algebraic
|
|
0
|
3
|
March 23, 2024
|
|
Separation Logic
|
|
0
|
4
|
March 23, 2024
|
|
Concrete Semantics
|
|
0
|
11
|
March 19, 2024
|
|
Semantic Domain blog
|
|
0
|
4
|
March 19, 2024
|
|
Why writing correct software is hard
|
|
0
|
7
|
March 19, 2024
|
|
Ghosts of departed proofs
|
|
0
|
4
|
March 19, 2024
|
|
Mathematics and Computation - Andrej Bauer's blog
|
|
0
|
4
|
March 19, 2024
|