Skip to content

Commit

Permalink
26Jun
Browse files Browse the repository at this point in the history
  • Loading branch information
Luís Soares Barbosa authored and Luís Soares Barbosa committed Jun 26, 2024
1 parent f5df898 commit 3e431b4
Show file tree
Hide file tree
Showing 2 changed files with 85 additions and 47 deletions.
Binary file added QL-Exer1-2023-24.pdf
View file
Binary file not shown.
132 changes: 85 additions & 47 deletions index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,18 +110,54 @@ <h5> T Lectures</h5>
<table style="width:100%">
<tr>
<td><strong>Feb 06 (11:00 - 13:00)</strong></td>
<td>Introduction to the course: objectives, learning outcomes, organisation.
<P>
The Curry-Howard-Lambek isomorphism for intuitionistic logic.</td>
<td>Introduction to the course: objectives, learning outcomes, organisation. Logic and (quantum) computation.
</td>
</tr>
<tr>
<td><strong>Feb 13 (11:00 - 13:00)</strong></td>
<td>...
<td> CARNIVAL
</td>
</tr>
<tr>
<td><strong>Feb 20 (11:00 - 13:00)</strong></td>
<td>Intuitionistic logic: formulae, sequents and proofs; natural deduction for intuitionistic logic; admissibility.
</td>
</tr>
<tr>
<td><strong>Feb 27 (11:00 - 13:00)</strong></td>
<td>Untyped lambda-calculus:(untyped) terms; alpha-equivalence; substitution; beta-reduction.
</td>
</tr>
<tr>
<td><strong>Mar 5 (11:00 - 13:00)</strong></td>
<td>Simply-typed lambda-calculus: types; (typed) terms; Curry-Howard-isomorphisms; beta-reduction; eta-reduction;
subject reduction; confluence; strong normalisation.
</td>
</tr>
<tr>
<td><strong>Mar 12 (11:00 - 13:00)</strong></td>
<td>Category theory: categories; monos and epis; isomorphisms; initial and terminal objects; products;
exponents; functors; natural transformations.
</td>
</tr>
<tr>
<td><strong>Mar 19 (11:00 - 13:00)</strong></td>
<td>Category theory (continued), categorical logic and intuitionistic linear logic: Yoneda lemma; adjoints; categorical semantics of simply-typed lambda calculus in Cartesian closed categories; soundness and completeness; intuitionistic linear logic.
</td>
</tr>
<tr>
<td><strong>Apr 2 (11:00 - 13:00)</strong></td>
<td>Linear and quantum lambda-calculi and monoidal categories: linear and quantum lambda-calculi; symmetric monoidal closed categories; categorical semantics of linear and quantum lambda-calculi.
</td>
</tr>
<tr>
<td><strong>Apr 9 (11:00 - 13:00)</strong></td>
<td>Linear and quantum lambda-calculi and monoidal categories: conclusion of the previous lecture. Closing of the course Module 1.
</td>
</tr>
<tr>
<td><strong>Apr 16 (11:00 - 13:00)</strong></td>
<td>Diagrams and categories. Diagramatic languages for processes.
<td>Introduction to module 2. Diagrams and categories. Diagramatic languages for processes.
Circuits <a href="LQ2324-Diagrams.pdf"> [lecture notes]</a>.
String diagrams: definitions, examples, constructions <a href="LQ2324-StringDiagrams.pdf"> [lecture notes]</a>.
</td>
Expand All @@ -143,57 +179,59 @@ <h5> T Lectures</h5>
</tr>
</table>



<!--
<li>
<strong>Mar 22 (11-13h):</strong>
Processes and diagrams. Monoidal categories and representation of process theories. Introduction to diagramatic reasoning.
</li>
<li>
<strong>Mar 29 (11-13h):</strong>
String diagrams. Non-separability. Representing transpose, trace, adjoint, conjugate and inner product.
</li>
<li>
<strong>Abr 5 (11-13h):</strong>
Unitary processes and projectors in string diagrams. Expressing quantum phenomena in theories interpreted over string diagrams (e.g. non cloning; teleportation). Dagger compact-closed categories.
</li>
<li>
<strong>Abr 19 (11-13h):</strong>
The process theory of linear maps: properties and constructions.
</li>
<li>
<strong>Abr 26 (11-13h):</strong>
F
</li>
<li>
<strong>May 03 (11-13h):</strong>
Introduction to the ZX-calculus. Examples.
[<a href="https://arxiv.org/abs/2012.13966">Tutorial by John van de Wetering (2020)</a>]
</li>
-->



<P>
<P><P><P><P>

<h5> TP Lectures </h5>


<table style="width:100%">
<tr>
<td><strong>Feb 06 (09:00 - 11:00)</strong></td>
<td>Practice on the Curry-Howard-Lambek isomorphism for intuitionistic logic.</td>
<td>Premiliminaries on logic and quentum computation.</td>
</tr>
<tr>
<td><strong>Feb 13 (09:00 - 11:00)</strong></td>
<td>...
<td>CARNIVAL
</td>
</tr>
<tr>
<tr>
<td><strong>Feb 20 (09:00 - 11:00)</strong></td>
<td>Intuitionistic logic: how to write proofs in natural deduction; how to show the admissibility of a rule.
</td>
</tr>
<tr>
<td><strong>Feb 27 (09:00 - 11:00)</strong></td>
<td>Untyped lambda-calculus: how to check if an expression is (not) a term; how to execute alpha-conversion and
beta-reduction.
</td>
</tr>
<tr>
<td><strong>Mar 5 (09:00 - 11:00)</strong></td>
<td>Simply-typed lambda-calculus: how to construct a term; how to execute beta- and eta-reductions.
</td>
</tr>
<tr>
<td><strong>Mar 12 (09:00 - 11:00)</strong></td>
<td>Category theory: how to prove that a concrete structure is a category; how to show that initial and
terminal objects as well as products are unique.
</td>
</tr>
<tr>
<td><strong>Mar 19 (09:00 - 11:00)</strong></td>
<td>Category theory (continued), categorical logic and intuitionistic linear logic: how to interpret some concrete terms; how to prove that a concrete structure is an adjoint; how to prove that exponents are right adjoints to products.
</td>
</tr>
<tr>
<td><strong>Apr 2 (09:00 - 11:00)</strong></td>
<td>Linear and quantum lambda-calculi and monoidal categories: how to write examples of linear and quantum terms; how to interpret examples of linear and quantum terms; how to prove an instance of a coherence theorem for monoidal categories.
</td>
</tr>
<tr>
<td><strong>Apr 9 (09:00 - 11:00)</strong></td>
<td>Linear and quantum lambda-calculi and monoidal categories: conclusion of the previous lecture.
</td>
</tr>
<tr>
<td><strong>Apr 16 (09:00 - 11:00)</strong></td>
<td>Exercises on circuits and string diagrams.
</td>
Expand Down Expand Up @@ -371,7 +409,7 @@ <h5><a name="Docente"></a> Lecturers </h5>
<h5><a name="Avaliação"></a> Assessment </h5>

<ul>
<li> Module 1: 6 take-home exercises + 1 written essay
<li> Module 1: 6 take-home exercises <a href="QL-Exer1-2023-24.pdf"> (pdf)</a> + 1 written essay
<li> Module 2: 2 take-home exercises <a href="LQ2324-Exercicios.pdf"> (pdf)</a> + 1 PyZX application essay
<li> Fianl grades <a href="Class23-24.pdf"> (here) </a>
</ul>
Expand All @@ -398,7 +436,7 @@ <h5><a name="Contacto"></a> Contacts </h5>
<li> Email: lsb arroba di ponto uminho ponto pt
<li> Appointments (Nori): Wed, 15:30-17:30 (please send an email the day before)
<li> Email: norihiro1988 arroba gmail ponto com
<li> Last update: 2024.06.24
<li> Last update: 2024.06.26
</ul>

<!--~~~~~~~~~~~~~~~~~~~~~~~-->
Expand All @@ -409,7 +447,7 @@ <h5><a name="Contacto"></a> Contacts </h5>

<div class="panel-footer" id="wrapper-footer">
<div id="footer">
2024.06.24
2024.06.26
</div>
</div>

Expand Down

0 comments on commit 3e431b4

Please sign in to comment.