Towards Dependently-Typed Control Effects (Extended Abstract) (TyDe 2022) - ICFP 2022

Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia

Who

Youyou Cong, Kenichi Asai

Track

Time Zone

The program is currently displayed in (GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague.

Use conference time zone: (GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, PragueSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Sun 11 Sep 2022 11:54 - 12:12 at Club CD - Tyde 2 Chair(s): Gabriel Scherer

Abstract

Dependent types and computational effects are indispensable for safe implementation of realistic programs. This abstract presents our ongoing work on designing a dependently-typed language with delimited control operators. We extend our previous language with conditionals whose branches may have different types and effects, and show how this language features makes it harder to type and CPS-translate programs.

File attachments

slides (tyde22.pdf)	476KiB

Youyou Cong

Tokyo Institute of Technology

Japan

Kenichi Asai

Ochanomizu University

Japan

Time Zone

The program is currently displayed in (GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague.

Use conference time zone: (GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, PragueSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Sun 11 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

	11:00 - 12:30	Tyde 2TyDe at Club CD Chair(s): Gabriel Scherer INRIA Saclay

	11:00 18m Short-paper		Idris2-Table: evaluating dependently-typed tables with the Brown Benchmark for Table Types (Extended Abstract) TyDe Robert Wright The University of Edinburgh, UK, Michel Steuwer University of Edinburgh, Ohad Kammar University of Edinburgh
	11:18 18m Short-paper		Syntax-Generic Operations, Reflectively Reified (Extended Abstract) TyDe Tzu-Chi Lin Institute of Information Science, Academia Sinica, Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica Pre-print
	11:36 18m Short-paper		Toward Grammar Inference via Refinement Types (Extended Abstract) TyDe Michael Schröder TU Wien, Jürgen Cito TU Wien Pre-print Media Attached
	11:54 18m Short-paper		Towards Dependently-Typed Control Effects (Extended Abstract)Virtual TyDe Youyou Cong Tokyo Institute of Technology, Kenichi Asai Ochanomizu University File Attached
	12:12 18m Full-paper		tylr, a tiny tile-based structure editor TyDe David Moon University of Michigan, Andrew Blinn University of Michigan, Cyrus Omar University of Michigan DOI Pre-print