scientific article; zbMATH DE number 733666
From MaRDI portal
Publication:4325974
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Information storage and retrieval of data (68P20) Specification and verification (program logics, model checking, etc.) (68Q60)
Recommendations
- Remarks on isomorphisms in typed lambda calculi with empty and sum types
- From semantics to types: the case of the imperative \(\lambda\)-calculus
- Isomorphisms of simple inductive types through extensional rewriting
- scientific article; zbMATH DE number 1701346
- scientific article; zbMATH DE number 1696613
- A short survey of isomorphisms of types
- scientific article; zbMATH DE number 512879
- Isomorphisms between the coherent models of the lambda-calculus
- Isomorphisms of types in the presence of higher-order references
- Type similarity for the Lambek-Grishin calculus revisited
Cited in
(29)- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Proof theory of higher-order equations: Conservativity, normal forms and term rewriting.
- A coinductive completeness proof for the equivalence of recursive types
- Efficient and flexible matching of recursive types
- Second order isomorphic types: A proof theoretic study on second order \(\lambda\)-calculus with surjective pairing and terminal object
- Functional pearl: the distributive \(\lambda\)-calculus
- Natural deduction systems for intuitionistic logic with identity
- Automorphisms of types and their applications
- Remarks on isomorphisms in typed lambda calculi with empty and sum types
- scientific article; zbMATH DE number 1696613 (Why is no real title available?)
- Automorphisms of types in certain type theories and representation of finite groups
- On the building of affine retractions
- Provable isomorphisms of types
- Cartesian isomorphisms are symmetric monoidal: A justification of linear logic
- Retrieving library functions by unifying types modulo linear isomorphism
- Normalisation of the TheoryTof Cartesian Closed Categories and Conservativity of ExtensionsT[x] ofT
- Remarks on isomorphisms of simple inductive types
- Procedural isomorphism, analytic information and -conversion by value
- An algebraic theory for web service contracts
- Using types as search keys in function libraries
- Proof normalisation in a logic identifying isomorphic propositions
- Extensional proofs in a propositional logic modulo isomorphisms
- Retrieving library identifiers via equational matching of types
- Topological quantum gates in homotopy type theory
- A note on synonymy in proof-theoretic semantics
- A type checker for a logical framework with union and intersection types (system description)
- Type isomorphisms for multiplicative-additive linear logic
- A verified framework for higher-order uncurrying optimizations
- Contract-based discovery of Web services modulo simple orchestrators
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4325974)
