• People
• Events
• Research

LFCS reports by Author: K

Kahn, Saif Ullah

• Machine Assisted Proofs for Generic Semantics to Compiler Transformation Correctness Theorems
  Saif Ullah Kahn
  LFCS report ECS-LFCS-97-379
  

Kahrs, Stefan

• Unlimp - Uniqueness as a Leitmotiv for Implementation
  Stefan Kahrs
  LFCS report ECS-LFCS-92-219
  
• Polymorphic Type Checking by Interpretation of Code
  Stefan Kahrs
  LFCS report ECS-LFCS-92-238
  
• Mistakes and Ambiguities in the Definition of Standard ML
  Stefan Kahrs
  LFCS report ECS-LFCS-93-257
  
• Interfaces and Extended ML
  Stefan Kahrs, Donald Sannella and Andrzej Tarlecki
  LFCS report ECS-LFCS-94-283
  
• First-Class Polymorphism for ML
  Stefan Kahrs
  LFCS report ECS-LFCS-94-284
  
• The Definition of Extended ML
  Stefan Kahrs, Donald Sannella, Andrzej Tarlecki
  LFCS report ECS-LFCS-94-300
  
• Towards a Domain Theory for Termination Proofs
  Stefan Kahrs
  LFCS report ECS-LFCS-95-314
  
• The definition of Extended ML: a gentle introduction
  Stefan Kahrs, Donald Sannella and Andrzej Tarlecki
  LFCS report ECS-LFCS-95-322
  
• Lecture Notes on Formal Program Development
  Stefan Kahrs
  LFCS report ECS-LFCS-97-372
  

Kaivola, Roope

• On modal mu-calculus and Büchi tree automata
  Roope Kaivola
  LFCS report ECS-LFCS-94-293
  
• Axiomatising Linear Time Mu-calculus
  Roope Kaivola
  LFCS report ECS-LFCS-95-324
  
• Using Automata to Characterise Fixed Point Temporal Logics
  Roope Kaivola
  LFCS report ECS-LFCS-97-356
  

Kazmierczak, Edmund

• Modularizing the Specification of a Small Database System in Extended ML
  E. Kazmierczak
  LFCS report ECS-LFCS-91-177
  
• Formal Program Development in Modular Prolog: A Case Study
  M Read and E Kazmierczak
  LFCS report ECS-LFCS-92-195
  

Kempster, Tim

• Diluting ACID
  Tim Kempster, Colin Stirling and Peter Thanisch
  LFCS report ECS-LFCS-99-404
  

Ketonen, J

• A Decision Procedure Revisited: Notes on Direct Logic, Linear Logic and its Implementations
  G Bellin and J Ketonen
  LFCS report ECS-LFCS-91-167
  

Khardon, Roni

• Learning Function Free Horn Expressions
  Roni Khardon
  LFCS report ECS-LFCS-98-394
  
• Learning Range Restricted Horn Expressions
  Roni Khardon
  LFCS report ECS-LFCS-98-395
  

Kick, Marco

• Coalgebraic Modelling of Timed Processes
  Marco Kick
  
  

Kinoshita, Yoshiki

• Lax naturality through enrichment
  Yoshiki Kinoshita and John Power
  LFCS report ECS-LFCS-95-330
  

Kirli, Dilsun

• Dynamic ML without Dynamic Types
  Stephen Gilmore, Dilsun Kirli and Christopher Walton
  LFCS report ECS-LFCS-97-378
  
• A Polymorphic Type and Effect System for Detecting Mobile Functions
  Dilsun Kirli
  LFCS report ECS-LFCS-99-413
  
• Mobile Computation with Functions
  Dilsun Kirli
  

Kleymann, Thomas

• Implementing Proof by Pointing without a Structure Editor
  Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira
  LFCS report ECS-LFCS-97-368
  
• Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs
  Thomas Kleymann
  LFCS report ECS-LFCS-98-392
  
• Metatheory of Verification Calculi in LEGO: To What Extent Does Syntax Matter?
  Thomas Kleymann
  LFCS report ECS-LFCS-98-393
  
• Hoare Logic and Auxiliary Variables
  Thomas Kleymann
  LFCS report ECS-LFCS-98-399
  

Knobel, Andreas

• Constructive lambda-Models
  Andreas Knobel
  LFCS report ECS-LFCS-90-120 (also published as CST-68-90)
  

Knoop, J

• Finite Constants: Characterizations of a new decidable set of constants
  B. Steffen and J. Knoop
  LFCS report ECS-LFCS-89-79
  

Kreig-Bruckner, Bernd

• Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL
  D. Sannella and B. Kreig-Bruckner
  LFCS report ECS-LFCS-91-135