Types for Proofs and Programs International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers /
Types for Proofs and Programs International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers / [electronic resource] :
edited by Thorsten Altenkirch, Wolfgang Naraschewski, Bernhard Reus.
- 1st ed. 1999.
- VIII, 212 p. online resource.
- Lecture Notes in Computer Science, 1657 1611-3349 ; .
- Lecture Notes in Computer Science, 1657 .
On Relating Type Theories and Set Theories -- Communication Modelling and Context-Dependent Interpretation: An Integrated Approach -- Gröbner Bases in Type Theory -- A Modal Lambda Calculus with Iteration and Case Constructs -- Proof Normalization Modulo -- Proof of Imperative Programs in Type Theory -- An Interpretation of the Fan Theorem in Type Theory -- Conjunctive Types and SKInT -- Modular Structures as Dependent Types in Isabelle -- Metatheory of Verification Calculi in LEGO -- Bounded Polymorphism for Extensible Objects -- About Effective Quotients in Constructive Type Theory -- Algorithms for Equality and Unification in the Presence of Notational Definitions -- A Preview of the Basic Picture: A New Perspective on Formal Topology.
9783540481676
10.1007/3-540-48167-2 doi
Computer science.
Machine theory.
Compilers (Computer programs).
Artificial intelligence.
Theory of Computation.
Computer Science Logic and Foundations of Programming.
Formal Languages and Automata Theory.
Compilers and Interpreters.
Artificial Intelligence.
QA75.5-76.95
004.0151
On Relating Type Theories and Set Theories -- Communication Modelling and Context-Dependent Interpretation: An Integrated Approach -- Gröbner Bases in Type Theory -- A Modal Lambda Calculus with Iteration and Case Constructs -- Proof Normalization Modulo -- Proof of Imperative Programs in Type Theory -- An Interpretation of the Fan Theorem in Type Theory -- Conjunctive Types and SKInT -- Modular Structures as Dependent Types in Isabelle -- Metatheory of Verification Calculi in LEGO -- Bounded Polymorphism for Extensible Objects -- About Effective Quotients in Constructive Type Theory -- Algorithms for Equality and Unification in the Presence of Notational Definitions -- A Preview of the Basic Picture: A New Perspective on Formal Topology.
9783540481676
10.1007/3-540-48167-2 doi
Computer science.
Machine theory.
Compilers (Computer programs).
Artificial intelligence.
Theory of Computation.
Computer Science Logic and Foundations of Programming.
Formal Languages and Automata Theory.
Compilers and Interpreters.
Artificial Intelligence.
QA75.5-76.95
004.0151