Experiments with NBE in Agda: full reduction and reduction of open terms. Extension of NBE to sums: meta-theoretical consequences, impossibility of a simple solution. A preview of delimited control operators and their operational and logical meanings. Intuitive explanation of Kripke models, and application of their model theory to showing underivability results for intuitionistic logic. Reading material corresponding to the lectures:
Homework: The file Day3.agda below contains an attempt at an extension of NBE to disjunction (sum types). Can you understand why a simple solution is not possible, and can you suggest how to overcome the problem by a computer program? No hand-ins are due, only discussion. |