Timely Computation - A Formal Approach to Digital Circuit Design
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a thought-provoking conference talk from ICFP 2023 that delves into the fundamental question of "what is a digital circuit?" in relation to the analog nature of physical circuits. Discover how speaker Conal Elliott presents a simple informal definition and formalizes it using the Agda proof assistant. Learn about the concept of timely embedding of discrete information in continuous signals and how it forms the basis for defining computational circuits. Examine the compositionally correct methodology that maintains specification, implementation, timing, and correctness proofs throughout the circuit design process. Gain insights into the algebraic vocabulary and homomorphisms used to support compositionality. Understand how key transformations reveal the linearity of circuit timing, enabling practical and modular verified timing analysis. Explore the emphasis on simplicity and generality in specifications, minimizing circuit-specific definitions while highlighting a broadly applicable methodology for scalable, compositionally correct engineering through denotations and homomorphisms.
Syllabus
[ICFP'23] Timely Computation
Taught by
ACM SIGPLAN
Related Courses
Logic: Language and Information 2University of Melbourne via Coursera Computation Structures - Part 1: Digital Circuits
Massachusetts Institute of Technology via edX Circuits and Electronics 3: Applications
Massachusetts Institute of Technology via edX Electrones en Acción: Electrónica y Arduinos para tus propios Inventos
Pontificia Universidad Católica de Chile via Coursera Basic Electronics
Indian Institute of Technology Bombay via Swayam