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
| Alabama A | Georgia Tech F | 10 | 0 | 0 | 10 |
| Auburn A | Tennesse B | 10 | 10 | 0 | 20 |
| Georgia Tech B | Auburn C | 10 | 10 | 0 | 20 |
| Georgia Tech A | Tusculum A | 10 | 10 | 0 | 20 |
| Clemson A | Georgia Tech C | 10 | 0 | 0 | 10 |
| Georgia Tech D | South Carolina A | 0 | 0 | 0 | 0 |
| Tennesse A | Georgia A | 10 | 0 | 0 | 10 |
| Haverford A | Lehigh A | 10 | 0 | 0 | 10 |
| Penn State B | Johns Hopkins B | 0 | 10 | 10 | 20 |
| Johns Hopkins A | Penn A | 10 | 10 | 10 | 30 |
| Penn State A | Rowan A | 10 | 0 | 0 | 10 |
| Rutgers C | Rutgers A | 10 | 0 | 0 | 10 |
| 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 |
| Ohio State C (DII) | CWRU D (DII) | 10 | 0 | 0 | 10 |
| Ohio State A (UG) | Kenyon A (UG) | 0 | 0 | 0 | 0 |
| Michigan A | Pitt B (UG) | 0 | 0 | 0 | 0 |
| Pitt A | Michigan B | 10 | 0 | 0 | 10 |
| Michigan State B (UG) | Michigan D (DII) | 10 | 0 | 0 | 10 |
| Kenyon B (DII) | Michigan State C (UG) | 10 | 0 | 0 | 10 |
| Ohio State B (DII) | CWRU C (UG) | 0 | 0 | 0 | 0 |
| Alberta | UBC B | 10 | 10 | 0 | 20 |
| UBC A | UW B | 10 | 10 | 0 | 20 |
| UW A | SFU | 10 | 0 | 0 | 10 |
| Bard A | Columbia A | 10 | 0 | 0 | 10 |
| Columbia B | Penn B | 10 | 0 | 0 | 10 |
| Emory A | Auburn B | 10 | 0 | 0 | 10 |