BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//TYPO3/NONSGML News system (news)//EN
BEGIN:VEVENT
UID:news-26528@cs.au.dk
DTSTAMP:20260826T134502Z
DTSTART:20260904T121500Z
DTEND:20260904T130000Z
END:VEVENT
END:VCALENDAR




<div class="news news-single">
	<div class="article" itemscope="itemscope" itemtype="http://schema.org/Article">
		
	
			<script type="text/javascript">
				const showAllContentLangToken = "Show all content ";
			</script>

			
			

			<article class="typo3-delphinus delphinus-gutters">

				<!-- News PID: 4980 - used for finding folder/page which contains the news / event -->
				<!-- News UID: 26528 - the ID of the current news / event-->

				<div class="news-event">
					<div class="news-event__header">
						<!-- Categories -->
						
							<span class="text--stamp">
<!-- categories -->
<span class="news-list-category">
	
		
	
		
	
		
	
		
	
		
	
		
	
</span>

</span>
						

						<!-- Title -->
						<h1 itemprop="headline">Inaugural Lecture by Daniel Gratzer</h1>
						
					</div>

					
						<!-- Top image -->
						
							

							<div class="news-event__hero-image" id="hero-image">
								<figure class="news-event__image">
									
									
											
													
	<picture>
		<source media="(max-width: 35.46em)" srcset="/fileadmin/_processed_/9/9/csm_Daniel-Gratzer-2024-web_345993b05e.jpg, /fileadmin/_processed_/9/9/csm_Daniel-Gratzer-2024-web_196b4c307d.jpg 1.5x">
		<img srcset="/fileadmin/_processed_/9/9/csm_Daniel-Gratzer-2024-web_b0cbd0263f.jpg 1.5x" itemprop="image" src="/fileadmin/_processed_/9/9/csm_Daniel-Gratzer-2024-web_eaa5940570.jpg" width="1370" height="1714" alt="" />
	</picture>

												
										

									<figcaption>
										
										
									</figcaption>
								</figure>
							</div>
						
					

					<div class="news-event__content">

						<!-- Events info box -->
						
								

								<div class="news-event__info theme--dark" id="event-info">
									<h2 class="screenreader-only">Info about event</h2>

									
											<!--- Same date -->
											<div class="news-event__info__item news-event__info__item--time">
												<h3 class="news-event__info__item__header text--label-header">Time</h3>
												<div class="news-event__info__item__content">
													<span class="u-avoid-wrap">
														Friday  4  September 2026,
													</span>
													<span class="u-avoid-wrap">
														&nbsp;at 14:15 -  15:00
													</span>
													<p class="news-event__info__item__ical-link"><a href="/news-events/events/show-event/artikel/inaugural-lecture-by-daniel-gratzer?tx_news_pi1%5Bformat%5D=ical&amp;type=9819&amp;cHash=9df8364f442beb513bc741038a1bfb98">Add to calendar</a></p>
												</div>
											</div>
										

									<!-- Location detailed -->
									
											<!-- Location Simple -->
											
												<div class="news-event__info__item">
													<h3 class="news-event__info__item__header text--label-header">Location</h3>
													<div class="news-event__info__item__content">
														<p>INCUBA Lille Aud., building 5510-104, Aabogade 15, 8200 Aarhus N</p>
													</div>
												</div>
											
										

									<!-- Organizer detailed -->
									
											<div class="news-event__info__item">
												<h3 class="news-event__info__item__header text--label-header">Organizer</h3>
												<div class="news-event__info__item__content">
													Department of Computer Science, Aarhus University
												</div>
												
													<div class="news-event__info__item__link">
														<a href="/">Åbogade 34, 8200 Aarhus N, Denmark.</a>
													</div>
												
											</div>
										

									<!-- Price -->
									

									<!-- Event link -->
									

									<!-- Registration -->
									
								</div>
							

						
							<!-- Media -->
							
								

	
	

	

	
		
				
				
					
				
			
	



							
						

						
							<div class="news-event__content__text">
								<span class="text--byline" id="byline">
									

									<!-- Author -->
									
										<span itemprop="author" itemscope="itemscope" itemtype="http://schema.org/Person">
											
													By
												

											
													<a href="mailto:mmd@cs.au.dk">
														<span itemprop="name">Mette Munch Dideriksen</span>
													</a>
												
										</span>
									
								</span>

								

									<!-- Body text -->
									<p><strong>Title</strong></p>
<p>Type theory, in and around computer science</p>
<p><strong>Abstract</strong></p>
<p>This talk concerns my work on type theory, a family of statically typed functional programming languages originally developed as a foundation for mathematics. This tension between "programming language" and "foundation for mathematics" has resulted in type theory's peculiar character, as well as its utility as the foundation for proof assistants like Rocq, Agda, and Lean. This talk has two goals. The first is to introduce type theory itself and gloss my expository work on this front. The second is to touch on the various flavours of type theory my research has explored as well as the uses to which they have been put.</p>
<p>----------------</p>
<p>Everyone is welcome!&nbsp;</p>
<p>There will be refreshments after the lecture.</p>
								
							</div>
						
					</div>

					
						<!-- Content elements -->
						
					
				</div>
			</article>

			
				
				
			

			<!-- related things -->
			
		

	</div>
</div>