Title: Introduction to Typed Lambda Calculus

Speaker: William DeMeo

Abstract: This is an introduction to the typed lambda calculus, a language for describing functions and tuples, with sum, product and function types. We briefly review the history and motivation of lambda calculus as an alternative to Turing machines. We discuss the syntax of lambda calculus and give some examples. Finally, we consider some reasons for choosing constructive type theory as a framework for doing math.

This is the first in a series of 6 meetings 3/28–4/1 (3 lectures at 11am and 3 hands-on practice sessions at 1:30pm).

(hands on exercise session; follow-up to 11am lecture on typed lambda calculus)

Title: Introduction to Type Theory

Speaker: William DeMeo

Abstract: Type Theory is a foundation for mathematics and computer science and was developed by logicians like Alonzo Church and Per Martin-Löf. Suitable as a basis for computer-assisted proof, it is receiving increasing interest from mathematicians (e.g., for verifying mathematical proofs) and computer scientists (e.g. for verifying compilers and operating systems). Type theory is based on the Curry-Howard Isomorphism, which describes a precise relationship between proofs of a proposition and programs of the corresponding type. In this brief course, we introduce the basics of Type Theory, and practice programming and proving in one of several software implementations of the theory.

(hands on practice session to accompany 11am lecture)

Speaker: Caleb Shor, Western New England University

Title: Characterization of free numerical semigroups

Abstract: Let $\mathbb{N}_0$ denote the set of nonnegative integers. A numerical semigroup $S$ is a subset of $\mathbb{N}_0$ that is closed under addition, contains 0, and has finite complement in $\mathbb{N}_0$. Such objects arise naturally in algebraic geometry and number theory. They’re also of interest to fans of postage stamps and chicken nuggets.

Given a set $G\subset\mathbb{N}_0$ with $\gcd(G)=1$, the set of nonnegative linear combinations of elements of $G$ is a numerical semigroup. It happens that every numerical semigroup arises this way, so we can think of numerical semigroups in terms of their generating sets. For example, if $G=\{3,5\}$, then $S=\{3x+5y : x,y\in\mathbb{N}_0\}=\mathbb{N}_0\setminus\{1,2,4,7\}$. In general, we will have $S=\mathbb{N}_0\setminus \textit{NR}(G)$, where $\textit{NR}(G)$ is the set of integers not representable in terms of $G$.

Numerous questions arise naturally. For instance, given a set $G$, what can we say about the cardinality, largest element, structure, and other associated objects and properties of $\textit{NR}(G)$? For a general set $G$, these can be difficult questions. In this talk, we will consider “free” numerical semigroups, which are generated by sets $G$ with certain smoothness conditions. In particular, we will see an identity which completely characterizes $\textit{NR}(G)$, and we will use that to answer some of the questions mentioned above.

Speaker: Vakhtang Putkaradze
Centennial Professor
Department of Mathematics and Statistics
Department of Chemical Engineering
PIMS Site Director at the University of Alberta

Title: Dynamics and control of flexible solar towers
Abstract:
The use of solar chimneys for energy production has been suggested more than 100 years ago. Unfortunately, this technology has not been realized on a commercial scale, in large part due to the high cost of erecting tall towers using traditional methods of construction. Recent works have suggested a radical decrease in tower cost by using an inflatable self-supported tower consisting of stacked toroidal bladders. While the statics deflections of such towers under constant wind have been investigated before, the key for further development of this technology lies in the analysis of dynamics, which is the main point of this talk. Using Lagrangian reduction by symmetry, we develop a fully three dimensional theory of motion for such towers and study the tower’s stability and dynamics. Next, we derive a geometric theory of optimal control for the tower dynamics using variable pressure inside the bladders, and perform detailed analytical and numerical studies of the control in two dimensions. Finally, we report on the results of experiments demonstrating the remarkable stability of the tower in real-life conditions, showing good agreement with theoretical results. This work has been supported by NSERC and the University of Alberta.

The Logic Seminar will meet again this Friday, usual place and time. The speaker will be Jack Yoon.

Title: Proof Mining

Abstract: Proof mining (proof unwinding) is a technique used to extract
constructive information from seemingly non-constructive proofs. We
discuss the idea behind the topic and describe the foundations which
form the basis for proof mining.