2 Assignments

Assignments will be posted here as the term progresses. Submission instructions are on the Marmoset page. Work is to be done individually. Please avoid excessive collaboration, and do not look for the answers to assignment questions on the Web or in other textbooks. Solutions will not be posted (this is a longstanding policy of mine, which I will be happy to explain to you).

In general, assignments will be finalized right after the corresponding chapter has been covered in lecture, and will be due roughly five to ten days later. There are no late submissions for credit (but if you need an extension, please contact me in advance with reasons). The starting point for each assignment is the "completed" file available on the Handouts page (but also linked here). You must do the exercises labelled "842 exercise". These are a mix of exercises from PLFA (some adapted) and exercises of my own. The exercises labelled "PLFA exercise" refer to exercises from PLFA that I have not chosen as assignment questions. Completing these is optional, and your solutions need not be included.

Please do not delete anything from the completed files (including comments). Of course, you can modify the line that includes the hole that is the starting point for your solution. Don’t change the imports unless you have advance permission from me. If you cannot complete an exercise, leave the incomplete solution in your file for possible partial credit. Just make sure that the file compiles (possibly with warnings about "unsolved metas" and "unsolved interaction metas").

Repeated Warning: The starter and completed files contain Unicode, which your browser is probably capable of displaying, but may not be configured to do so. Do not cut and paste from your browser. Instead, download the files using Command-click, Control-click, or right-click, depending on your system.

842Naturals.agda (due Sep. 16)
Exercises: Exponentiation (1), Increment (1), To/From (2), BinAdd (2).
Total: 6.

842Induction.agda (due Sep. 23)
Exercises: AddSwap (1), AddDistMult (2), MultAssoc (2), MultComm (3), LeftMonusZero (1), MonusAssocish (2), DoubleB (1), FromInc (1), FromToB (1), ToFromB (2), DblBInc (1), ToDbl (1), FromDblB (1), BinPlusLInc (2), PlusUnaryBinary (2).
Total: 23.

842Relations.agda (due Sep. 30)
Exercises: LTTrans (1), Trichotomy (2), LEtoLTS (1), LEStoLT (1), LTtoSLE (1), LTStoLE (1), OPOE (2). Total: 9.

There are no exercises associated with 842Equality.agda.

842Isomorphism.agda (due Oct. 7)
Exercises: IncCanOne (2), OneInc (1), CanToB (1), OneDblbX0 (1), OneToFrom (3), CanToFrom (1), OneUnique (2), CanUnique (1), IsoNCanR (3). Total: 15.

842Connectives.agda (due Oct. 11)
Exercises: IffIsoIfOnlyIf (1), SumCommIso (1), SumAssocIso (1), EmptyLeftIdIso (1), EmptyRightIdIso (1), ImpProdRightDist (1), ImpSumLeftDist (1), SumOfProdImpProdOfSum (1). Total: 8.

842Negation.agda (due Oct. 21)
Exercises: NotFourLTThree (1), LTIrrefl (1), LTTrich (3). Total: 5.

842Quantifiers.agda (due Oct. 25)
Exercises: ForAllDistProd (1), SumForAllImpForAllSum (1), ExistsDistSum (2), ExistsProdImpProdExists (1), AltLE (3), ExistsNegImpNegForAll (1). Total: 9.

842Decidable.agda (due Oct. 28)
Exercises: DecLT (3), DecNatEq (3), ErasBoolDec (removed 2019), ErasIFF (3). Total: 9.

842Lists.agda (due Nov. 1)
Exercises: RevCommApp (1), RevInvol (1), MapCompose (1), MapAppendComm (1), FoldrOverAppend (1), MapIsFoldr (1), Foldl (1), FoldrMonFoldl (2). Total: 9.

842Lambda.agda (due Nov. 13)
Exercises: NatMul (1), ChurchMul (1), StepEmbedsIntoStepPrime (2), MulTyped (2), MulCTyped (2). Total: 8.

842Properties.agda (due Nov. 20)
Exercises: AltProg (5), ValueEh (1), Unstuck (3). Total: 9.

There are no exercises associated with 842DeBruijn.agda.

842More.agda (due Nov. 27)
Exercises: SumsEmpty (10). Total: 10.

842Inference.agda (due date to be announced, probably Dec. 3)
Exercises: NatMul (1), ChurchMul (1), DecideBidirect (5), Decorate (3), ToTerm (2), ontoTerm (3), ontoBidir (5, bonus). Total: 15+5.

There are no exercises associated with 842Untyped.agda.