---
tags: 論文メモ
---

# Lem: reusable engineering of real-world semantics

## 背景

### 問題意識
- シスプロの文脈でも形式的手法が浸透してきてよいが,でかいモデルをつくるとメンテナンスがダルい・再利用可能性が低いなどがある
- proof assistant lock-in
- 定理証明支援系は学習コストが高いので一度特定のツールを使うことにするとなかなか移行できない
- 特に依存型→LCFみたいなのは移植がほぼ無理

### 問題への貢献
- Lem: 単一の仕様記述言語から複数の定理証明支援系/プログラム言語上の定義への変換(portable definition), 可視化latex/html
- 各定義が変換された先で同じ意味ををもつことは保証されない

## 具体的な手法など