On Choice Rules in Dependent Type Theory

DOI10.1007/978-3-319-55911-7_2zbMath1435.68065OpenAlexW2598762888MaRDI QIDQ2988806

Maria Emilia Maietti

Publication date: 19 May 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11577/3234330

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Type theory (03B38)

Related Items (2)

The compatibility of the minimalist foundation with homotopy type theory ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)

Uses Software

• Coq
• Matita

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quotient completion for the foundation of constructive mathematics
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Realizability. An introduction to its categorical side
• A minimalist two-level foundation for constructive mathematics
• Constructivism in mathematics. An introduction. Volume I
• Sheaves in geometry and logic: a first introduction to topos theory
• Independence of the induction principle and the axiom of choice in the pure calculus of constructions
• Unifying exact completions
• Elementary quotient completion
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• The Matita Interactive Theorem Prover
• An extensional Kleene realizability semantics for the Minimalist Foundation

This page was built for publication: On Choice Rules in Dependent Type Theory