The effects of effects on constructivism

DOI10.1016/J.ENTCS.2019.09.006OpenAlexW2995889279WikidataQ113317357 ScholiaQ113317357MaRDI QIDQ2133168FDOQ2133168

Authors: Liron Cohen, Sofia Abreu Faro, Ross Tate 

Publication date: 29 April 2022

Full work available at URL: https://doi.org/10.1016/j.entcs.2019.09.006

Recommendations

• Countable Choice as a Questionable Uniformity Principle
• scientific article; zbMATH DE number 1795226
• Choice Principles and Constructive Logics†
• The fundamental theorem of algebra: a constructive development without choice.
• scientific article; zbMATH DE number 1670500

zbMATH Keywords

effectsnon-determinismcountable choiceconstructivismstateful computation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites Work

• Innovations in computational type theory using Nuprl
• Constructivism in mathematics. An introduction. Volume I
• Categorical logic and type theory
• Tripos theory in retrospect
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Tripos theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Notions of computation and monads
• Title not available (Why is that?)
• On the interpretation of intuitionistic number theory
• Constructive set theory
• Title not available (Why is that?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• Realizability. An introduction to its categorical side
• On the computational content of the axiom of choice
• Categorical set theory: A characterization of the category of sets
• Title not available (Why is that?)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Title not available (Why is that?)
• Some axioms for constructive analysis
• On the Cauchy completeness of the constructive Cauchy reals
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proofs as programs
• Title not available (Why is that?)
• A system of axiomatic set theory. Part III. Infinity and enumerability. Analysis
• Title not available (Why is that?)
• History of constructivism in the 20th century
• A weak countable choice principle
• Title not available (Why is that?)
• Countable Choice as a Questionable Uniformity Principle
• Title not available (Why is that?)
• Computability beyond Church-Turing via choice sequences
• The effects of effects on constructivism
• A sequent calculus with dependent types for classical arithmetic

Cited In (2)

• The effects of effects on constructivism
• Stateful Realizers for Nonstandard Analysis

Uses Software

• Nuprl
• Agda

This page was built for publication: The effects of effects on constructivism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2133168)