Summer School on the Proofs-as-Programs Paradigm