Questions tagged [curry-howard]

The tag has no usage guidance.

2 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
1
vote
0answers
79 views

Equality Theorems with Type Theoretic Proof

I am investigating how I might be able to translate even commonplace equalities/ inequalities via the so-called Curry-Howard Correspondance - from a generic, set theoretic plus AOC foundation - into a ...
-1
votes
0answers
48 views

Differences in the type signatures using dependent types

What is the difference between the following types for the $head$ function on a vector of integers. ($head$ takes a natural number $n$ and a vector $v$ of length $n$ or $(n+1)$ (depending on the ...