Progamming construct as corresponding (ir of ) logic
October 14, 2022 —
sameer
# Progamming construct as corresponding (ir of ) logic
| logic | construct |
| linear | rust borrow checker , cbpv |
| double negation, classical | csp, cbpv |
| mu calculus | call cc |
| system f | stlc + parametric polymorphism |
| modus ponens | eval map |
| material implication, currying adjunction | exponential object |
| tautology | terminal object has a global preposition |
| modality | provability in axiom-K |
| modus ponens : resolution | substitution,subtyping, function application |
| ch, aoc | imcrecdicative |
| skolem, unification, sequent | tebleaux prolog |
| modal logic | referential transparency |
| modal algebra | boolean algebra + unary op |
| prepositional | invariant in bisimulation |
| fol | no normal forms |
| terms:lamda calc to combinatory logic | ch-deduction meta theorem |
| tt | Property |
| mltt | everything terminates |
Tags: logic, agda, rust, curry-howard