Question
The Curry–Howard isomorphism states that computer programs are directly equivalent to these mathematical constructs, which can be automated using the languages Lean or Rocq (“rock”). For 10 points each:
[10e] Name these mathematical constructs that are used to formally demonstrate the truth of a mathematical statement.
ANSWER: mathematical proofs [or formal proofs or proofs of correctness; accept proof assistant or theorem prover or Rocq prover]
[10m] According to the Curry–Howard isomorphism, these programming concepts correspond to individual propositions of a proof. One method of “inferring” these things in programming languages like Python is named for the duck test.
ANSWER: data types [accept type inference or duck typing]
[10h] Haskell Curry also lends his name to “currying,” a common tool in functional programming languages that transforms a function into a sequence of functions each with a smaller value for this property. A description is acceptable.
ANSWER: arity [accept descriptions of the number of arguments or the number of parameters or the number of inputs of a function]
<Other Science>
Summary
| 2024 ACF Winter at Clemson | 2024-11-16 | Y | 8 | 12.50 | 88% | 38% | 0% |
| 2024 ACF Winter at Lehigh | 2024-11-16 | Y | 7 | 14.29 | 86% | 29% | 29% |
| 2024 ACF Winter at Northwestern | 2024-11-16 | Y | 9 | 15.56 | 78% | 56% | 22% |
| 2024 ACF Winter at Ohio State | 2024-11-16 | Y | 7 | 5.71 | 57% | 0% | 0% |
| 2024 ACF Winter at UBC | 2024-11-16 | Y | 3 | 16.67 | 100% | 67% | 0% |
Data
| Indiana A | WashU B | 10 | 10 | 10 | 30 |
| UChicago D | Miami | 10 | 0 | 0 | 10 |
| Northwestern A | Purdue C | 10 | 10 | 0 | 20 |
| UChicago B | UChicago A | 10 | 0 | 0 | 10 |
| UIUC A | Purdue A | 10 | 10 | 10 | 30 |
| UIUC B | UChicago C | 0 | 10 | 0 | 10 |
| Purdue B | UIUC C | 0 | 10 | 0 | 10 |
| UIUC D | Purdue D | 10 | 0 | 0 | 10 |
| WashU D | WashU C | 10 | 0 | 0 | 10 |