Implementing Cantor’s Paradise

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

zbMATH Keywords

coalgebrasparadoxeslogical frameworkshyperuniversesFitch-Prawitz set theory

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Related Items (1)

LF+ in Coq for "fast and loose" reasoning

Uses Software

• Coq
• Twelf
• Agda
• LLFp

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