scientific article; zbMATH DE number 3331288
From MaRDI portal
Publication:5610115
zbMath0208.20101MaRDI QIDQ5610115
Publication date: 1970
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (42)
The Girard-Reynolds isomorphism ⋮ A unified approach to type theory through a refined \(\lambda\)-calculus ⋮ Understanding uniformity in Feferman's explicit mathematics ⋮ The calculus of constructions ⋮ Automath Type Inclusion in Barendregt’s Cube ⋮ Innovations in computational type theory using Nuprl ⋮ Supporting the formal verification of mathematical texts ⋮ Type theory and formalisation of mathematics ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge ⋮ Size-based termination of higher-order rewriting ⋮ The Girard-Reynolds isomorphism (second edition) ⋮ Characteristics of de Bruijn’s early proof checker Automath ⋮ A scalable module system ⋮ What does logic have to tell us about mathematical proofs? ⋮ Revisiting the notion of function ⋮ Expressing computational complexity in constructive type theory ⋮ Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project ⋮ Representing model theory in a type-theoretical logical framework ⋮ POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE ⋮ Preface to the special volume ⋮ Representing Model Theory in a Type-Theoretical Logical Framework ⋮ Intuitionistic categorial grammar ⋮ An introduction to univalent foundations for mathematicians ⋮ Combinatorial topology and constructive mathematics ⋮ Inductive-data-type systems ⋮ Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician ⋮ Inherited extension of many-sorted theories ⋮ A note on complexity measures for inductive classes in constructive type theory ⋮ Telescopic mappings in typed lambda calculus ⋮ Typing and computational properties of lambda expressions ⋮ From constructivism to computer science ⋮ Towards a computation system based on set theory ⋮ A general proof certification framework for modal logic ⋮ NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF ⋮ On principal types of combinators ⋮ Programs as proofs: A synopsis ⋮ Realizability and intuitionistic logic ⋮ A proof description language and its reduction system ⋮ PlatΩ: A Mediator between Text-Editors and Proof Assistance Systems ⋮ Towards semantic mathematical editing ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
Uses Software
This page was built for publication:
