The effects of effects on constructivism
From MaRDI portal
Publication:2133168
DOI10.1016/j.entcs.2019.09.006OpenAlexW2995889279WikidataQ113317357 ScholiaQ113317357MaRDI QIDQ2133168
Ross Tate, Liron Cohen, Sofia Abreu Faro
Publication date: 29 April 2022
Full work available at URL: https://doi.org/10.1016/j.entcs.2019.09.006
Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Uses Software
Cites Work
- Some axioms for constructive analysis
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Notions of computation and monads
- Innovations in computational type theory using Nuprl
- Realizability. An introduction to its categorical side
- Constructivism in mathematics. An introduction. Volume I
- Categorical logic and type theory
- Categorical set theory: A characterization of the category of sets
- The effects of effects on constructivism
- A Constructive Proof of Dependent Choice, Compatible with Classical Logic
- Tripos theory in retrospect
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Proofs as programs
- Tripos theory
- Constructive set theory
- On the computational content of the axiom of choice
- A weak countable choice principle
- Countable Choice as a Questionable Uniformity Principle
- On the Cauchy Completeness of the Constructive Cauchy Reals
- Computability Beyond Church-Turing via Choice Sequences
- A sequent calculus with dependent types for classical arithmetic
- A system of axiomatic set theory. Part III. Infinity and enumerability. Analysis
- On the interpretation of intuitionistic number theory
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
