Implementing Cantor’s Paradise
From MaRDI portal
Publication:3179294
DOI10.1007/978-3-319-47958-3_13zbMath1485.03031OpenAlexW2528085415MaRDI QIDQ3179294
Marina Lenisa, Furio Honsell, Luigi Liquori, Ivan Scagnetto
Publication date: 21 December 2016
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01362819/file/FitchCameraReady.pdf
Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Light linear logic
- A general construction of hyperuniverses
- A category of compositional domain-models for separable Stone spaces.
- An open logical framework
- The consistency problem for positive comprehension principles
- PREDICATE AND SET-THEORETIC CALCULI BASED ON LOGIC WITHOUT CONTRACTIONS
- A framework for defining logics
- $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
- General Recursion via Coinductive Types
- Fast and loose reasoning is morally correct
- Combining proofs and programs in a dependently typed language
- An introduction to (co)algebra and (co)induction
- Types for Proofs and Programs
- A demonstrably consistent mathematics—Part I
This page was built for publication: Implementing Cantor’s Paradise