Peter Dybjer (Chalmers University), Tests, games, and Martin-Löf's meaning explanations for intuitionistic type theory.
Schedule
- Feb. 13, 2012, 14:00 - 15:00
Abstract
In this talk I shall argue that program testing provides the basis for constructive mathematical truth. This point of view leads to a modification of Martin-Löf's meaning explanations for intuitionistic type theory, where the judgements of type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. In particular we get a new interpretation of hypothetical judgments, since tests for such judgments need methods for generating inputs. We sketch a "test manual" for intuitionistic type theory which employs concepts from game semantics, for example, input generation corresponds to opponent's moves in a game. In order to test a typing judgement we simultaneously play a strategy generated by a type and a strategy generated by a term, where the correct moves for the strategy of the term are determined dynamically by playing the strategy of the type.
The talk is on joint work in progress with Pierre Clairambault, Cambridge.
Attachments
In this talk I shall argue that program testing provides the basis for constructive mathematical truth. This point of view leads to a modification of Martin-Löf's meaning explanations for intuitionistic type theory, where the judgements of type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. In particular we get a new interpretation of hypothetical judgments, since tests for such judgments need methods for generating inputs. We sketch a "test manual" for intuitionistic type theory which employs concepts from game semantics, for example, input generation corresponds to opponent's moves in a game. In order to test a typing judgement we simultaneously play a strategy generated by a type and a strategy generated by a term, where the correct moves for the strategy of the term are determined dynamically by playing the strategy of the type.
The talk is on joint work in progress with Pierre Clairambault, Cambridge.