patternModerate
Daily Applications of Type Theory
Viewed 0 times
typetheoryapplicationsdaily
Problem
I want to understand type theory but I have to know first how I can apply it. Could there be more non-obvious applications of type theory aside from in type systems in programming? Could there be other applications, let's say in personality profiling and the likes?
Solution
Because of the Curry-Howard correspondence, types can be interpreted as propositions, and propositions as types.
As a result of this, type theory is applicable to literally any field that uses formal logic for its proofs. This can be circuit verification, real analysis, symbolic logic, geometry, etc.
For instance, some automated proof checking tools work using this principle: they check the validity of the proof by type-checking a particular term in some type system. The LF proof checker is based on this approach, as is HOL Light. As an example application, proof-carrying-code used LF to check proofs of memory-safety of untrusted code. The benefit of using this kind of proof-checker is that the implementation can be very simple, and thus we can gain high assurance that the implementation is correct. See, e.g., the following paper:
Foundational Proof Checkers with Small Witnesses. Dinghao Wu, Andrew W. Appel, Aaron Stump. PPDP 2003.
As a result of this, type theory is applicable to literally any field that uses formal logic for its proofs. This can be circuit verification, real analysis, symbolic logic, geometry, etc.
For instance, some automated proof checking tools work using this principle: they check the validity of the proof by type-checking a particular term in some type system. The LF proof checker is based on this approach, as is HOL Light. As an example application, proof-carrying-code used LF to check proofs of memory-safety of untrusted code. The benefit of using this kind of proof-checker is that the implementation can be very simple, and thus we can gain high assurance that the implementation is correct. See, e.g., the following paper:
Foundational Proof Checkers with Small Witnesses. Dinghao Wu, Andrew W. Appel, Aaron Stump. PPDP 2003.
Context
StackExchange Computer Science Q#48754, answer score: 11
Revisions (0)
No revisions yet.