Constructive mathematics and computer programming
From MaRDI portal
Cited in
(51)- HasCasl: integrated higher-order specification and program development
- Possible forms of evaluation or reduction in Martin-Löf type theory
- Constructing recursion operators in intuitionistic type theory
- Generalized algebraic theories and contextual categories
- On the syntax of Martin-Löf's type theories
- Algebra of constructions. I. The word problem for partial algebras
- The calculus of constructions
- About primitive recursive algorithms
- Type checking with universes
- A bridge between constructive logic and computer programming
- Program development in constructive type theory
- An intuitionistic theory of types with assumptions of high-arity variables
- Constructing type systems over an operational semantics
- Nonconstructive computational mathematics
- Representing scope in intuitionistic deductions
- From constructivism to computer science
- System \(T\), call-by-value and the minimum problem
- Process calculus based upon evaluation to committed form
- Well-ordering proofs for Martin-Löf type theory
- Computational foundations of basic recursive function theory
- Realizability interpretation of generalized inductive definitions
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- A constructive approach to state description semantics
- Analogical program derivation based on type theory
- Extraction and verification of programs by analysis of formal proofs
- Towards a computation system based on set theory
- The Girard-Reynolds isomorphism
- The axioms of constructive geometry
- Foundational aspects of multiscale digitization
- From LCF to Isabelle/HOL
- Inverse semigroups with apartness
- Axiomatizing geometric constructions
- Indexed induction-recursion
- One step is enough
- Failure of normalization in impredicative type theory with proof-irrelevant propositional equality
- scientific article; zbMATH DE number 53194 (Why is no real title available?)
- Constructive Mathematics in Theory and Programming Practice
- Computational logic: its origins and applications
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe
- The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
- The RedPRL proof assistant (invited paper)
- Tableaux for automated reasoning in dependently-typed higher-order logic
- Extended bar induction in applicative theories
- Functorial polymorphism
- Innovations in computational type theory using Nuprl
- The Girard-Reynolds isomorphism (second edition)
- Proof-theoretical analysis: Weak systems of functions and classes
- Do-it-yourself type theory
- Domain interpretations of Martin-Löf's partial type theory
- Formal methods in the philosophy of science
This page was built for publication: Constructive mathematics and computer programming
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3343983)
