311 citations · 1.2k across the 38 of their papers we have counts for
6 papers · 1 filter
Towards an induction principle for nested data types
Peng Fu, Peter Selinger
A well-known problem in the theory of dependent types is how to handle so-called nested data types. These data types are difficult to program and to reason about in total dependent…
Dependently Typed Folds for Nested Data Types
Peng Fu, Peter Selinger
We present an approach to develop folds for nested data types using dependent types. We call such folds , they have the following properties. (1)…
Applying quantitative semantics to higher-order quantum computing
Michele Pagani, Peter Selinger, Benoît Valiron
Finding a denotational semantics for higher order quantum computation is a long-standing problem in the semantics of quantum programming languages. Most past approaches to this pro…
Lecture notes on the lambda calculus
Peter Selinger
This is a set of lecture notes that developed out of courses on the lambda calculus that I taught at the University of Ottawa in 2001 and at Dalhousie University in 2007 and 2013.…
A linear-non-linear model for a computational call-by-value lambda calculus (extended abstract)
Peter Selinger, Benoît Valiron
We give a categorical semantics for a call-by-value linear lambda calculus. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming lang…
A lambda calculus for quantum computation with classical control
Peter Selinger, Benoit Valiron
The objective of this paper is to develop a functional programming language for quantum computers. We develop a lambda calculus for the classical control model, following the first…