The Foundations Group / Brouwer Institute Seminar Series
Please contact the organizers Alexandra Silva or Josef Urban in case you are interested in giving a talk.
Past Seminars and Special Events
voorjaar 2013 |
Time |
Room |
Speaker |
Institution |
Title |
Tue May 28 |
13.30--14:30 |
HG02.028 |
Bas Spitters |
RU |
Modal Type Theory |
Tue May 21 |
13.30--14:30 |
HG00.303 |
Prakash Panagaden |
McGill U. |
Stone Duality for Markov Processes |
Tue May 14 |
13.30--14:30 |
HG02.028 |
Bas Spitters |
RU |
Real Numbers in Homotopy Type Theory |
Tue May 7 |
13.30--14:30 |
HG02.028 |
Egbert Rijke |
RU |
Higher Inductive Types |
Tue 30 apr |
13.30--14:30 |
HG02.028 |
Queen's day |
|
|
Tue 23 apr |
13.30--14:30 |
HG02.028 |
no seminar |
|
|
Tue 16 apr |
13.30--14:30 |
HG02.028 |
Robbert Krebbers |
RU |
Exploring the formal proof of Feit-Thompson |
Tue 9 apr |
14.30--15:30 |
HG01.029 |
Josef Urban |
RU |
AI over Large Formal Knowledge Bases: The First Decade |
Tue 2 apr |
13.30--14:30 |
HG02.028 |
Herman Geuvers |
|
|
Tue 26 mar |
13.30--14:30 |
HG02.028 |
no seminar (Freek Verbek's defense in the Aula, see also symposium next day) |
|
|
Tue 19 mar |
13.30--14:30 |
HG02.028 |
no seminar |
|
|
Tue 12 mar |
13.30--14:30 |
HG02.028 |
Freek Wiedijk |
RU |
Should proof assistants be used to verify absence of overflow? |
Tue 5 mar |
13.30--14:30 |
HG02.028 |
no seminar - COIN at CWI |
|
|
Tue 26 feb |
13.30--14:30 |
HG02.028 |
Evgeni Makarov |
RU |
Separation Logic for a Functional Language |
Tue 19 feb |
13.30--14:30 |
HG02.028 |
Daniel Gebler |
VU |
Compositionality of Approximate and Metric Bisimulation in Probabilistic Transition Systems |
Tue 12 feb |
13.30--14:30 |
HG02.028 |
no seminar |
|
|
Tue 5 feb |
13.30--14:30 |
HG02.028 |
no seminar |
|
|
Tue 29 jan |
13.30--14:30 |
HG02.028 |
Josef Urban |
RU |
BliStr: The Blind Strategymaker |
Tue 22 jan |
13.30--14:30 |
HG02.032 |
Herman Geuvers |
RU |
De Bruijn's ideas on the Formalization of Mathematics |
Tue 15 jan |
13.30--14:30 |
HG02.028 |
Henning Basold |
CWI |
Co-Banach - How to avoid something |
najaar 2012 |
Time |
Room |
Speaker |
Institution |
Title |
Tue 11 dec |
13.30--14:30 |
HG02.028 |
|
|
|
Tue 11 dec |
13.30--14:30 |
HG02.028 |
|
|
|
Tue 4 dec |
13.30--14:30 |
HG02.028 |
Jasmin Blanchette |
TU Munchen |
Foundational, Compositional (Co)datatypes for Higher-Order Logic (Category Theory Applied to Theorem Proving) |
Tue 27 nov |
13:35--15:00 |
HG02.028 |
Egbert Rijke and Bas Spitters |
RU |
In homotopy type theory, do hsets form a predicative topos? |
Tue 20 nov |
13.30--14:30 |
HG01.058 |
Robbert Krebbers |
RU |
Separation Logic for Non-local Control Flow |
Tue 13 nov |
13.30--14:30 |
|
|
|
no seminar |
Tue 6 nov |
13.30--14:30 |
HG02.028 |
Carst Tankink |
RU |
Editing programs, editing proofs - A guided tour |
Tue 30 oct |
13.30--14:30 |
HG03.054 |
Helle Hvid Hansen |
RU |
Brzozowski revisited: minimal language acceptors via dual adjunctions |
Tue 23 oct |
13.30--14:30 |
HG03.054 |
Egbert Rijke and Bas Spitters |
RU |
In homotopy type theory, do hsets form a predicative topos? |
Tue 16 oct |
13.30--14:30 |
HG03.054 |
Andrew Polonski |
RU |
Turing-complete typed systems of arithmetic |
Tue 9 oct |
13.30--14:30 |
HG03.054 |
Herman Geuvers |
RU |
Extracting a search algorithm from a classical proof |
Tue 2 oct |
13.30--14:30 |
HG03.054 |
Alexandra Silva |
RU |
Brzozowski's algorithm (co)algebraically |
Tue 25 sep |
13:30-14:30 |
HG03.054 |
Tessa Matser |
RU |
The Curry-Howard isomorphism for classical logic |
Tue 18 sep |
15:00--16:00 |
HG01.060 |
Hans Zantema |
TUE/RUN |
Cinderella and the wicked Stepmother, or how to avoid overflow |
Wed 22 aug |
14.30--15.30 |
HG02.028 |
Cezary Kaliszyk |
University of Innsbruck |
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora |
voorjaar 2012 |
Time |
Room |
Speaker |
Institution |
Title |
Tue 19 jun |
15.30--17:30 |
HG00.071 |
Jade Alglave |
University of Oxford |
Fences in Weak Memory Models |
Tue 19 jun |
10.45--11:45 |
HG02.702 |
Dexter Kozen |
Cornell University |
Program constructs for non-well-founded computation |
Tue 12 jun |
10.45--11:45 |
HG02.702 |
Michael Beeson |
San Jose State University |
Triangle Tiling |
Tue 5 jun |
10.45--11:45 |
|
no seminar ( COIN on Monday) |
|
|
Tue 29 may |
10.45--11:45 |
HG02.702 |
Freek Wiedijk |
RU |
tba |
Tue 22 may |
10.45--11:45 |
|
no seminar |
|
|
Tue 15 may |
10.45--11:45 |
HG02.702 |
Andrew Polonski |
RU |
Church--Rosser via Standardization |
Tue 8 may |
10.45--11:45 |
|
|
|
no seminar |
Tue 1 may |
10.45--11:45 |
|
|
|
no seminar |
Tue 24 apr |
10.45--11:45 |
HG02.702 |
Pieter Collins |
Maastricht U. |
Validated Function Calculus and Applications to Hybrid Systems |
Tue 17 apr |
10.45--11:45 |
HG02.702 |
Robbert Krebbers |
RU |
|
Tue 10 apr |
10.45--11:45 |
HG02.702 |
Jelle Herold |
RU |
|
Tue 3 apr |
10.45--11:45 |
HG02.702 |
Carst Tankink |
RU |
|
Tue 27 mar |
10.45--11:45 |
HG02.702 |
Cyril Cohen |
INRIA |
A construction of the discrete field of real algebraic numbers in Coq |
Tue 20 mar |
10.45--11:45 |
HG01.029 |
Bas Spitters |
RU |
From computational analysis to thoughts about analysis in Homotopy type theory |
Tue 13 mar |
10.45--11:45 |
HG02.702 |
Freek Wiedijk |
RU |
The next generation of proof assistants: ten questions |
Tue 6 mar |
10.45--12:15 |
HG02.702 |
Ken Madlener |
RU |
Mathematical Operational Semantics in Coq |
Tue 28 feb |
10.45--12:15 |
HG02.702 |
Steffen van Bakel |
Imperial College London, UK |
|
Tue 21 feb |
10.45--12:15 |
HG02.702 |
|
|
no seminar |
Tue 14 feb |
10.45--12:15 |
HG02.702 |
Freek Verbeek |
OU/RU |
Using ACL2 for the Formal Verification of on-Chip Communication Fabrics |
Tue 7 feb |
10.45--12:15 |
HG02.702 |
Henk Barendregt |
RU |
|
Tue 31 jan |
10.45--12:15 |
HG01.029 |
Bas Joosten |
OU |
|
Mon 23 jan |
13:30--16:00 |
HG00.086 |
|
|
seminar merged with COIN on Monday |
Tue 17 jan |
15.45--17:00 |
HG02.028 |
Hans Zantema |
TUE/RUN |
Type preservation and confluence in simply typed lambda calculus by abstract reduction techniques |
najaar 2011 |
Time |
Room |
Speaker |
Institution |
Title |
Tue 20 dec |
15.45--17:00 |
HG02.028 |
|
|
no seminar |
Tue 13 dec |
15.45--17:00 |
HG01.028 |
Josef Urban |
RUN |
ATP and Presentation Service for Mizar |
Tue 6 dec |
15.45--17:00 |
HG02.028 |
|
|
no seminar -- Sinterklaas |
Tue 29 nov |
15.45--17:00 |
HG02.028 |
Hans Zantema |
TUE/RUN |
Type preservation in simply typed lambda calculus by abstract reduction techniques |
Tue 22 nov |
15.45--17:00 |
HG02.028 |
Joerg Endrullis / Dimitri Hendriks |
VU |
|
Tue 15 nov |
15.45--17:00 |
HG02.028 |
|
|
no seminar - ICT.Open |
Tue 8 nov |
15.45--17:00 |
HG02.028 |
Wouter Swierstra (organizer) |
RUN |
Collective exploration of the VSTTE 2012 Software Verification Competition |
Tue 1 nov |
15.45--17:00 |
HG02.028 |
James McKinna |
|
Autumn leaves from Shonan Village |
Tue 25 oct |
15.45--17:00 |
HG02.028 |
|
|
no seminar |
Tue 18 oct |
15.45--17:00 |
HG02.028 |
Carst Tankink |
RUN |
Proofs are Documents, and Movies too! |
Tue 11 oct |
15.45--17:00 |
HG02.028 |
Robbert Krebbers |
RUN |
Formalizing the C99 Standard |
Tue 4 oct |
15.45--17:00 |
HG02.028 |
Wouter Swierstra |
RUN |
From math to machine: a formal derivation of an executable Krivine machine |
Tue 27 sep |
15.45--17:00 |
HG02.028 |
Jesse Alama |
New University of Lisbon |
Generalizing Theorems of the Mizar Mathematical Library by Type Promotion and Property Omission |
Tue 20 sep |
15.45--17:00 |
HG02.028 |
Bas Joosten |
RUN |
Ampersand |
Tue 13 sep |
15.45--17:00 |
HG02.028 |
Sebastian Reichelt |
RUN |
Ideas for a MathWiki Editor |
Tue 6 sep |
15.45--17:00 |
|
|
|
no seminar |
Tue 30 aug |
15:45--17:00 |
HG02.028 |
Lionel Mamane |
RUN |
Dependencies in Coq |
voorjaar 2011 |
Time |
Room |
Speaker |
Institution |
Title |
Tue 21 jun (TBC) |
15.45--17:00 |
HG02.028 |
Andrew Polonsky |
VU |
|
Tue 17 mei |
15.45--17:00 |
HG02.028 |
Twan van Laarhoven |
RUN |
|
Tue 10 mei |
13:30--15:30 |
HG02.028 |
Rudolf Mak; Joost Winter |
TU/e; CWI |
streams seminar Periodic-Drop-Take Calculus for Stream Transformers; Context-free languages and streams |
Tue 03 mei |
|
|
|
|
no seminar: meivakantie |
Tue 26 apr |
15.45--17:00 |
HG00.065 |
Carst Tankink |
RUN |
|
Tue 19 apr |
15.45--17:00 |
HG02.028 |
|
|
no seminar |
Tue 12 apr |
|
|
|
|
no seminar |
Tue 05 apr |
15.45--17:00 |
HG02.028 |
Pierre Letouzey |
PPS/INRIA |
|
Tue 29 mar |
15.45--17:00 |
HG02.028 |
Wouter Swierstra |
RUN |
Adventures in Extraction Verifying XMonad |
Tue 22 mar |
15.45--17:00 |
HG02.028 |
Robbert Krebbers |
RUN |
|
Tue 15 mar |
|
|
|
|
no seminar |
Tue 08 mar |
|
|
|
|
no seminar: Carneval |
Tue 01 mar |
15.45--17:00 |
HG02.028 |
Bas Joosten |
U.Twente/RUN |
|
Tue 22 feb |
10.30--12:30 |
HG00.023 |
Frits Dannenberg; Franz Staals |
TU Delft; TU/e |
streams seminar Toeplitz substitutions and transducer equivalence; Stream equality in Coq |
Tue 15 feb |
15.45--17:00 |
HG02.028 |
Wouter Swierstra (TBC) |
RUN |
Agda Tutorial |
Tue 08 feb |
15.45--17:00 |
HG02.028 |
Daniel Kuhlwein |
RUN |
|
Tue 01 feb |
15.30--17:00 |
HG02.028 |
Sebastian Reichelt |
|
|
Tue 25 jan |
13.30--15:30 |
HG02.032 |
Wieb Bosma |
RUN |
streams seminar: Automatic Sequences |
Tue 18 jan |
15:30--16:45 |
HG02.028 |
Josef Urban |
RUN |
trip report: AMS Special Session on Formal Mathematics for Mathematicians |
najaar 2010 |
Time |
Room |
Speaker |
Institution |
Title |
Tue 21 dec |
|
|
|
|
no seminar: Kleene Coalgebra Day |
Thu 16 dec |
15:30--17:00 |
HG00.308 |
Jakob Rehof |
Dortmund |
|
Tue 14 dec |
15.30--16.45 |
HG02.028 |
Henk Barendregt |
RUN |
Five Easy Pieces, pt II |
Tue 07 dec |
15.30--16.45 |
HG02.028 |
Jesse Alama |
New University of Lisbon |
|
Tue 30 nov |
15.30--16.45 |
HG02.028 |
|
|
no seminar (see below) |
Tue 30 nov |
13.30--15:30 |
HG00.065 |
Wouter Swierstra/Diana Koenraadt |
|
streams seminar: Stream Fusion/Equality and unicity by bisimulation |
Tue 23 nov |
|
|
|
|
no seminar |
Tue 16 nov |
15.30--16.45 |
HG00.058 |
Josef Urban |
RUN |
A Wiki for Mizar etc. |
Tue 09 nov |
15.30--16.45 |
HG00.058 |
Giulio Manzonetto |
RUN |
Resource Calculi II: Full Abstraction for Resource Calculus with Tests |
Tue 02 nov |
15.30--16.45 |
HG00.058 |
Robbert Krebbers |
RUN |
afstudeerpraatje: Classical logic, control calculi and data types |
Mon 01 nov |
13:30--15:30 |
HG00.065 |
Herman Geuvers/Eelis vd Weegen |
RUN |
streams seminar: Representations of real numbers |
Tue 26 okt |
|
|
|
|
no seminar |
Tue 19 okt |
15.30--16.45 |
HG00.058 |
Hans Zantema |
TU/e |
|
Tue 12 okt |
15.30--16.45 |
HG00.058 |
Kasper Brink |
RUN |
|
Tue 05 okt |
15.30--16.45 |
HG01.058 |
Henk Barendregt |
RUN |
Five Easy Pieces, pt I |
Mon 04 okt |
13:30--15:30 |
HG00.065 |
Joerg Endrullis/Hans Zantema |
TU/e |
streams seminar: Tools proving equality of streams |
Tue 28 sep |
15.30--16.45 |
HG01.058 |
Giulio Manzonetto |
RUN |
Resource Calculi: some syntax, some semantics |
Tue 21 sep |
|
|
|
|
no seminar |
Wed 15 sep |
15.30--16.45 |
HG00.062 |
Iris Loeb |
VU |
The Layers of Tarski's Foundations of the Geometry of Solids |
Tue 14 sep |
15.30--16.45 |
HG01.028 |
Wouter Swierstra |
RUN |
|
Mon 06 sep |
13:30--15:30 |
HG00.065 |
Jan Rutten/Milad Niqui |
RUN/CWI |
streams seminar: Stream differential equations |
voorjaar 2010 |
Time |
Room |
Speaker |
Institution |
Title |
Tue 13 jul |
|
|
|
|
no seminar: papers at ITP/UITP@FLoC, Edinburgh |
Tue 06 jul |
15:30--16:45 |
HG03.082 |
Olha Shkaravska |
RUN |
Univariate Polynomial Solutions of Nonlinear Polynomial Recurrence Relations |
Tue 29 jun |
|
|
|
|
no seminar |
Tue 22 jun |
15:30--16:45 |
HG03.082 |
Cezary Kaliszyk |
TUM |
|
Mon 21 jun |
14:00--16:00 |
HG02.028 |
Bas Spitters |
RUN |
streams seminar: Quantification over streams |
Tue 15 jun |
15:30--16:45 |
HG03.082 |
Thomas Forster |
DPMMS, Cambridge |
|
Tue 08 jun |
15:30--16:45 |
HG03.082 |
James McKinna |
RUN |
Realisability in Chambery: trip report |
Tue 01 jun |
|
|
|
|
no seminar |
Tue 25 mei |
|
|
|
|
no seminar |
Tue 18 mei |
15:30--16:45 |
HG03.082 |
Peter Hancock |
MSP group, Strathclyde |
|
Mon 17 mei |
14:00--16:00 |
HG02.028 |
Peter Hancock |
MSP group, Strathclyde |
|
Tue 11 mei |
15:30--16:45 |
HG01.058 |
James McKinna |
RUN |
Type inference in context: Algorithm W, revisited |
Tue 04 mei |
|
|
|
|
no seminar: meivakantie |
Tue 27 apr |
|
|
|
|
no seminar |
Tue 20 apr |
|
|
|
|
streams seminar: Klop, Hendricks, Endrullis |
Tue 13 apr |
|
|
|
|
no seminar |
Tue 06 apr |
|
|
|
|
no seminar: FLoC deadlines |
Tue 30 mar |
15:30--16:45 |
HG01.058 |
Bas Spitters |
RUN |
Spitters and vd Weegen, ptIII |
Tue 23 mar |
15:30--16:45 |
HG01.058 |
Bas Spitters |
RUN |
Spitters and vd Weegen, ptII |
Tue 16 mar |
15:30--16:45 |
HG01.058 |
Bas Spitters |
RUN |
The algebraic hierarchy using type classes in type theory ptI |
Tue 09 mar |
|
|
|
|
not assigned yet |
Tue 02 mar |
15:30--16:45 |
HG01.058 |
Josef Urban |
RUN |
Mizar, Automated Reasoning, and Artificial Intelligence (part 2) |
Tue 23 feb |
15:30--16:45 |
HG01.058 |
Jesse Alama |
Centro de Inteligência Artificial, Universidade Nova de Lisboa |
Expressibility of some properties of finite combinatorial polyhedra in FOL and extensions |
Tue 16 feb |
|
|
|
|
no seminar: Carnaval |
Tue 09 feb |
15:30--16:45 |
HG01.058 |
Josef Urban |
RUN |
ISLA 2010 and Mizar workshop talk |
Tue 02 feb |
15:30--16:45 |
HG01.058 |
Herman Geuvers |
RUN |
najaar 2009 |
Time |
Room |
Speaker |
Institution |
Title |
Tue 08 Dec |
15:30--16:45 |
HG01.058 |
Robbert Krebbers |
RUN |
|
Tue 17 Nov |
15:30--16:45 |
HG01.058 |
Hans Zantema |
TU/e, RUN |
|
Tue 10 Nov |
|
|
|
|
no seminar |
Tue 03 Nov |
|
|
|
|
no seminar: onderzoekvisitatie |
Tue 28 Okt |
|
|
|
|
no seminar: herfstvakantie |
Tue 21 Okt |
15:30--16:45 |
HG01.058 |
Bas Spitters |
RUN |
|
Tue 14 Okt |
15:30--16:45 |
HG01.058 |
Freek Wiedijk |
RUN |
report on Dagstuhl seminar Two faces of deduction |
Wed 07 Okt |
15:30--16:45 |
HG02.032 |
Cezary Kaliszyk |
TUM |
Lifting type properties to properties of equivalence classes in Isabelle/HOL |
Tue 06 Okt |
15:30--16:45 |
Gymnasion GN2 |
O'Connor jury |
various |
|
Mon 05 Okt |
13:30--14:30 |
Aula |
Russell O'Connor |
McMaster University |
thesis defence |
Tue 29 Sep |
15:30--16:45 |
HG01.058 |
Freek Wiedijk |
RUN |
rehearsal: Dagstuhl talk Two automation challenges |
Tue 22 Sep |
15:30--16:45 |
HG01.058 |
Allan van Hulst |
RUN |
A Mizar Formalisation of the Schroeder-Bernstein Theorem in a weak Set Theory |
Tue 15 Sep |
15:30--16:45 |
HG01.058 |
Herman Geuvers |
RUN |
Trip report on CSL 2009 |
Tue 08 Sep |
15:30--16:45 |
HG01.058 |
Lionel Elie Mamane |
Gestman, Debian, cypherpunks.lu, L² Transfinite Technologies, ... |
Trip report on DML2009 workshop |
Tue 01 Sep |
15:30--16:45 |
HG01.058 |
Freek Wiedijk |
RUN |
Trip report on TPHOLs2009 and ITP workshop |