Abstract Semi-simplicial and semi-cubical sets are commonly defined as presheaves over, respectively, the semi-simplex or semi-cube category. Homotopy type theory then popularized an alternative definition, where the set of $n$ -simplices or $n$ -cubes are instead regrouped into the families of the fibers over their faces, leading to a characterization we call indexed. Moreover, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds parametricity, respectively, in their unary and binary variants. We exploit this correspondence to develop an original uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, and fully formalize it in Coq.

We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an "intensional" or "effective" view of respectively ill- and well-foundedness properties to an "extensional" or "ideal" view of these properties. After classifying and analysing the relations between different intensional definitions of ill-foundedness and well-foundedness, we introduce, for a domain A, a codomain B and a "filter" T on finite approximations of functions from A to B, a generalised form GDCABT of the axiom of dependent choice and dually a generalised bar induction principle GBIABT such that:GDCABTintuitionistically captures the strength of·the general axiom of choice expressed as ∀a∃bR(a,b) ⇒ ∃α∀aR(a,α(a))) when T is a filter that derives point-wise from a relation R on A × B without introducing further constraints,·the Boolean Prime Filter Theorem / Ultrafilter Theorem if B is the two-element set \mathbbB (for a constructive definition of prime filter),·the axiom of dependent choice if A = \mathbbN,·Weak Knig's Lemma if A = \mathbbN and B = \mathbbB (up to weak classical reasoning).GBIABTintuitionistically captures the strength ofGödel's completeness theorem in the form validity implies provability for entailment relations if B = \mathbbB (for a constructive definition of validity),·bar induction if A = \mathbbN,·the Weak Fan Theorem if A = \mathbbN and B = \mathbbB.Contrastingly, even though GDCABT and GBIABTsmoothly capture several variants of choice and bar induction, some instances are inconsistent, e.g. when A is \mathbbB\mathbbNand B is \mathbbN.

The call-by-need evaluation strategy for the λ-calculus is an evaluation strategy that lazily evaluates arguments only if needed, and if so, shares computations across all places where it is needed. To implement this evaluation strategy, abstract machines require some form of global environment. While abstract machines usually lead to a better understanding of the flow of control during the execution, facilitating in particular the definition of continuation-passing style translations, the case of machines with global environments turns out to be much more subtle.

This paper presents a dependently-typed construction of semi-simplicial sets in a type theory where sets are taken to be types. This addresses an open question raised on the wiki of the special year on Univalent Foundations at the Institute of Advanced Study (2012–2013).

No abstract available.

Martin-Löf's type theory has strong existential elimination (dependent sum type) that allows to prove the full axiom of choice. However the theory is intuitionistic. We give a condition on strong existential elimination that makes it computationally compatible with classical logic. With this restriction, we lose the full axiom of choice but, thanks to a lazily-evaluated coinductive representation of quantification, we are still able to constructively prove the axiom of countable choice, the axiom of dependent choice, and a form of bar induction in ways that make each of them computationally compatible with classical logic.

Abstract Pure Type Systems are usually described in two different ways, one that uses an external notion of computation like beta-reduction, and one that relies on a typed judgment of equality, directly in the typing system. For a long time, the question was open to know whether both presentations described the same theory. A first step towards this equivalence has been made by Adams for a particular class of Pure Type Systems (PTS) called functional. Then, his result has been relaxed to all semi-full PTSs in previous work. In this paper, we finally give a positive answer to the general question, and prove that equivalence holds for any Pure Type System.

We design an intuitionistic predicate logic that supports a limited amount of classical reasoning, just enough to prove a variant of Markov's principle suited for predicate logic. At the computational level, the extraction of an existential witness out of a proof of its double negation is done by using a form of statically-bound exception mechanism, what can be seen as a direct-style variant of Friedman's A-translation.

There are two usual ways to describe equality in a dependent typing system, one that uses an external notion of computation like beta-reduction, and one that introduces a typed judgement of beta-equality directly in the typing system. After being an open problem for some time, the general equivalence between both approaches has been solved by Adams for a class of pure type systems (PTSs) called functional. In this paper, we relax the functionality constraint and prove the equivalence for all semi-full PTSs by combining the ideas of Adams with a study of the general shape of types in PTSs. As one application, an extension of this result to systems with sub-typing would be a first step toward bringing closer the theory behind a proof assistant such as Coq to its implementation.

We show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al's call-by-value calculus of delimited control, an extension of λμ-calculus with delimited control known to be equationally equivalent to Danvy and Filinski's calculus with shift and reset. Our main result then is that de Groote and Saurin's variant of λμ-calculus is equivalent to a canonical call-by-name variant of Ariola et al's calculus. The rest of the paper is devoted to a comparative study of the call-by-name and call-by-value variants of Ariola et al's calculus, covering in particular the questions of simple typing, operational semantics, and continuation-passing-style semantics. Finally, we discuss the relevance of Ariola et al's calculus as a uniform framework for representing different calculi of delimited continuations, including "lazy" variants such as Sabry's shift and lazy reset calculus.

Abstract The historical design of the call-by-value theory of control relies on the reification of evaluation contexts as regular functions and on the use of ordinary term application for jumping to a continuation. To the contrary, the control calculus, developed by the authors, distinguishes between jumps and terms . This alternative calculus, which derives from Parigot's λμ-calculus, works by direct structural substitution of evaluation contexts. We review and revisit the legacy theories of control and argue that provides an observationally equivalent but smoother theory. In an additional note contributed by Matthias Felleisen, we review the story of the birth of control calculi during the mid- to late-eighties at Indiana University.

There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters (prompts), the continuations become composable and the calculi are believed to become more expressive. We formalise that the addition of prompts corresponds to the addition of a single dynamically-scoped variable modelling the special top-level continuation. From a type perspective, the dynamically-scoped variable requires effect annotations. From a logic perspective, the effect annotations can be understood in a standard logic extended with the dual of implication, namely subtraction.

We consider reducibility sets defined not by induction on types but by induction on sequents as a tool to prove strong normalization of systems with explicit substitution. To illustrate this point, we give a proof of strong normalization (SN) for simply‐typed call‐by‐name λ̄μμ̃‐calculus enriched with operators of explicit unary substitutions. The λ̄μμ̃‐calculus, defined by Curien and Herbelin, is a variant of λμ‐calculus with a let operator that exhibits symmetries such as terms/contexts and call‐by‐name/call‐by‐value reduction.

We present the μ -calculus, a syntax for λ-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived from implicational Gentzen's sequent calculus LK, a key classical logical system in proof theory. Under the Curry-Howard correspondence between proofs and programs, we can see LK, or more precisely a formulation called LKμ , as a syntax-directed system of simple types for μ -calculus. For μ -calculus, choosing a call-by-name or call-by-value discipline for reduction amounts to choosing one of the two possible symmetric orientations of a critical pair. Our analysis leads us to revisit the question of what is a natural syntax for call-by-value functional computation. We define a translation of λμ-calculus into μ -calculus and two dual translations back to λ-calculus, and we recover known CPS translations by composing these translations.

The interaction processes at work by M. Hyland and L. Ong (1994) (HO) and S. Abramsky et al. (1994) (AJM) new game semantics are two preexisting paradigmatic implementations of linear head reduction: respectively Krivine's abstract machine and Girard's interaction abstract machine. There is a simple and natural embedding of AJM-games to HO-games, mapping strategies to strategies and reducing AJM definability (or full abstraction) property to HO's one.

Abstract We present here a generalization of A-translation to a class of pure type systems. We apply this translation to give a direct proof of the existence of a looping combinator in a large class of inconsistent type systems, a class which includes type systems with a type of all types. This is the first non-automated solution to this problem.