`Travelled to:`

1 × Brazil

1 × France

1 × Germany

2 × Denmark

3 × Italy

3 × USA

`Collaborated with:`

D.Kapur S.Schupp D.Gregor J.V.Guttag A.Vargun S.Liu R.W.Erickson ∅ A.A.Stepanov E.Horowitz R.Agarwal X.Nie

`Talks about:`

proof (3) type (3) transform (2) librari (2) tecton (2) system (2) specif (2) rewrit (2) induct (2) data (2)

## Person: David R. Musser

### DBLP: Musser:David_R=

### Contributed to:

### Wrote 12 papers:

- SAC-2008-VargunM
- Code-carrying theory (AV, DRM), pp. 376–383.
- CC-2001-SchuppGML #generative #type system
- User-Extensible Simplification — Type-Based Optimizer Generators (SS, DG, DRM, SML), pp. 86–101.
- GCSE-2001-GregorSM #injection
- Base Class Injection (DG, SS, DRM), pp. 106–117.
- SCAM-2001-SchuppGM #library
- Library Transformations (SS, DG, DRM), pp. 111–123.
- SCAM-J-2001-SchuppGML02 #behaviour #library #semantics
- Semantic and behavioral library transformations (SS, DG, DRM, SML), pp. 797–810.
- RTA-1991-AgarwalMKN #proving
- The Tecton Proof System (RA, DRM, DK, XN), pp. 442–444.
- LICS-1986-KapurM #induction #reasoning #specification
- Inductive Reasoning with Incomplete Specifications (DK, DRM), pp. 367–377.
- ICALP-1982-GuttagKM #term rewriting #tool support
- Derived Pairs, Overlap Closures, and Rewrite Dominoes: New Tools for Analyzing Term rewriting Systems (JVG, DK, DRM), pp. 300–312.
- PS-1981-KapurMS #named
- Tecton: A Language for Manipulating Generic Objects (DK, DRM, AAS), pp. 402–414.
- CADE-1980-EricksonM #proving #scalability #theorem proving
- The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs (RWE, DRM), pp. 220–231.
- POPL-1980-Musser #data type #induction #on the #proving
- On Proving Inductive Properties of Abstract Data Types (DRM), pp. 154–162.
- ICSE-1976-GuttagHM #data type #design #specification
- The Design of Data Type Specifications (JVG, EH, DRM), pp. 414–420.