- Multi-staged programming language
Staged computation, which explicitly divides a computation into
separate stages, is a unifying framework for existing program
generation systems: partial evaluation, run-time code generation,
function inlining and macro expansion are all instances of staged computation.
Recently, I am interested in type system, Curry-Howard correspondence,
exception analysis, and unstaging transformation of open-code multi-staged
programming languages.
- Program analyzer generating system
We address two problems in compiling high-level static
analysis specifications into executable analyzers: how to check the
correctness - termination - of the specifications and
how to achieve the efficiency of the generated analyzers.
One of the sufficient conditions for terminating program analysis
is the extensionality of analysis function.
Once extensionality of the function is ascertained, the
generated analyzer is guaranteed to terminate.
In order to achieve the efficiency of the generated analyzers,
we develop a differential fixpoint iteration method.
-
Static Extensivity Analysis for Lambda-Definable Functions Over Lattices
Hyunjun Eo,
Kwangkeun Yi,
Kwang-Moo Choe
New Generation Computing
(in revision)
-
A Differential Fixpoint Iteration Method for Static Analysis Specifications
Hyunjun Eo,
Kwangkeun Yi
Technical Memorandum
ROPAS-2004-21,
Research On Program Analysis System,
Seoul National University, February 2004.
-
An Improved Differential Fixpoint Iteration Method for Program Analysis
Hyunjun Eo,
Kwangkeun Yi
In Proceedings of
The Third Asian Workshop on Programming Languages and Systems,
Shanghai Jiao Tong University, Shanghai, November 2002.
-
Static Extensionality Analysis for Lambda-Definable Functions Over Lattices
Kwangkeun Yi,
Hyunjun Eo
In Proceedings of
The Third Asian Workshop on Programming Languages and Systems,
Shanghai Jiao Tong University, Shanghai, November 2002.
-
Static Extensionality Analysis for Lambda-Definable Functions Over Lattices
Kwangkeun Yi,
Hyunjun Eo
Technical Memorandum
ROPAS-2002-17,
Research On Program Analysis System,
National Creative Research Center,
Korea Advanced Institute of Science and Technology, September 2002.
-
분석기 생성 시스템 Z1에서 그래픽 사용자 인터페이스의 자동 생성
어현준,
이광근,
김성훈
한국정보과학회 97 봄 학술발표논문집,
(24)1:57-60, 1997년 4월.
-
분석기 생성 시스템 Z1에서 그래픽 사용자 인터페이스의 자동 생성
어현준
석사학위논문,
KAIST, 1998
-
SUIF program analysis using System Z2
Seong-Hoon Kim,
Kwangkeun Yi,
Hyun-jun Eo,
Kwang-Moo Choe
In Proceedings of
The 2nd SUIF Workshop, 185-190,
Stanford Univ. 21-23 August 1997.
- Type system and type based program analysis
-
Proofs of a Set of Hybrid Let-Polymorphic Type Inference Algorithms
Hyunjun Eo,
Oukseh Lee,
Kwangkeun Yi
New Generation Computing
Vol. 22, No.1, pp.1-36, 2004.
-
Static Extensivity Analysis for Lambda-Definable Functions Over Lattices
Hyunjun Eo,
Kwangkeun Yi,
Kwang-Moo Choe
New Generation Computing
Vol. 24, No. 1, pp. 53-78, 2006
-
Type and Effect System for Multi-Staged Exceptions
Hyunjun Eo,
Ik-Soon Kim,
Kwangkeun Yi
In Proceedings of
The 4th Asian Symposium on Programming Languages and Systems (APLAS '2006),
Sydney, November 2006.
Lecture Notes in Computer Science, Vol. 4279, pp. 61-78.
- Fixpoint iteration algorithm
- Model checking and program logic
-
Proofs about Folklore: Why Model Checking = Reachability?
Nikolay V. Shilov,
Kwangkeun Yi,
Hyunjun Eo,
Seung-Hwan O,
Kwang-Moo Choe
Acta Informatica,
(submitted)
-
Game Semantics with Finite Plays for Propositional Program Logics
Hyunjun Eo,
Seung-Hwan O,
Nikolay V. Shilov
(submitted to)
Computer Science Logic (CSL '2005)
-
Finite Game Semantics for Propositional Program Logics
Hyunjun Eo,
Seung-Hwan O,
Nikolay V. Shilov
Short Presentation in
The Twentieth Annual IEEE Symposium on Logic in Computer Sciece (LICS '2005)
,
Chicago, June 2005.
-
모델체커를 검증하기 위한 모델체커
어현준,
Nikolay V. Shilov,
이광근
한국정보과학회 가을학술회의,
28(2):337-339, 2001년 10월.
- Run-time specialzation of static analysis
We present a technique of using static analysis for estimating
program's input-dependent properties.
A static analysis that is originally designed for estimating the
input-independent properties of programs is transformed into one that
can safely estimate the input-dependent properties at
the programs' input occurrence.
Our idea is to defer the finish of the static analysis to the
program's run-time. By analyzing the static analysis, we identify the
parts of the analysis that are sensitive to the program's inputs, hence need
to be deferred to the program's run-time. Then by using an analysis
named static value-slicing, we short-cut some of the dynamic
parts so that they are solved by simple membership
tests for the program's input. This re-formulation
accelerates the analysis; once the program's input occurs the prepared
dynamic parts can immediately and simultaneously start to resolve.
-
실행시간 전문화를 위한 집합기반분석의 준비
어현준,
이광근
한국정보과학회 논문지,
27(9):986-1002, 2000년 9월.
-
Preparing Set-Based Analysis for Run-time Specialization
Hyunjun Eo,
Kwangkeun Yi
Technical Memorandum
ROPAS-1999-1,
Research On Program Analysis System,
National Creative Research Center,
Korea Advanced Institute of Science and Technology, November 1999.
-
정적 분석의 실행시간 전문화에 관한 연구
어현준,
이광근
프로그래밍언어연구회
1999년 동계 워크샵 논문집, 1999년 2월.
(slides)
- Etc.
-
nML 컴파일러 시스템 (status report)
이광근,
이욱세,
어현준,
김정택,
최웅식,
류석영,
강현구,
서선애,
장성순,
김범식
한국정보과학회 가을학술회의,
28(2):340-342, 2001년 10월.
-
Standard ML에서 처리되지 않은 예외상황의 발생된 위치를 출력하는 방법
어현준
학사학위논문,
KAIST, 1996