Building formal proofs is made easier by tools called proof assistants. In this thesis we present the process of building a proof assistant for propositional intuitionistic linear logic. Linear logic is a refinement of classical and intuitionistic logic which puts its main focus on the role of its formulas as resources. While the consumption of formulas as if they are resources is a big advantage of linear logic that other logics do not offer, it is also a burden when trying to build proofs. Resource allocation in rules like Tensor Right is a difficult task since we need to predict where resources are going to be used by the rest of the proof before building it. Previous work by Hodas and Miller presents a way of using Input-Output contexts to work around this issue. But because we are building a proof-assistant and not an automated theorem prover, we need to allow the user to be able to switch between goals at any time, and be able to construct the proof in any order they want, so we cannot solve the problem with such contexts. We tackle this problem by allowing unbounded context growth when moving up the proof derivation tree, and instead allowing terms to only use variables from a given resources multiset which is a subset of the whole context. These subsets then have to satisfy a given set of equations that make them suitable for simulating context splittings and changes. In order to allow for incremental proof construction we use meta variables to stand for incomplete terms and modal contexts to store said variables, which builds on previous work by Nanevski et al. We define two sequent calculi, a base one, and one that represents the implementation. We present a cut admissibility proof that proves that our base sequent calculus is consistent, as well as a theorem which shows that every proof in the implementation calculus, has a proof in the base calculus as well.
"},{"label":"Degree","value":["Bachelor of Arts with Departmental Honors"]},{"label":"Administrative Note","value":"2017