著者

本多 健太郎 角谷 良彦 久保田 貴大

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.31, no.4, pp.4_9-4_20, 2014-10-24 (Released:2014-12-24)

著者

角谷 良彦

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.25, no.1, pp.1_167-1_179, 2008 (Released:2008-02-29)

---

本論文では,直観主義様相論理IKにCurry-Howard対応する名前呼び及び値呼びの計算系を提案する.名前呼び計算は,圏論的意味論に基づいており,単純型付き名前呼びλ-計算の拡張となっている.本論文は,名前呼び計算の簡約系が強正規化可能性及び合流性を持つことを証明する.また,値呼び計算は,値呼びのλ-計算として定評のあるλc-計算の拡張として定義される.名前呼びの場合と同様,値呼び計算に対しても簡約系を与え,その強正規化可能性及び合流性を証明する.加えて,本論文では,値呼び計算の部分体系が名前呼び計算へのCPS変換によって特徴付けられることを示す.最後に,様相論理IS4への計算系の拡張についても考察する.

著者

角谷 良彦

出版者

Japan Society for Software Science and Technology

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.25, no.1, pp.167-179, 2008

---

本論文では,直観主義様相論理IKにCurry-Howard対応する名前呼び及び値呼びの計算系を提案する.名前呼び計算は,圏論的意味論に基づいており,単純型付き名前呼びλ-計算の拡張となっている.本論文は,名前呼び計算の簡約系が強正規化可能性及び合流性を持つことを証明する.また,値呼び計算は,値呼びのλ-計算として定評のあるλ_c-計算の拡張として定義される.名前呼びの場合と同様,値呼び計算に対しても簡約系を与え,その強正規化可能性及び合流性を証明する.加えて,本論文では,値呼び計算の部分体系が名前呼び計算へのCPS変換によって特徴付けられることを示す.最後に,様相論理IS4への計算系の拡張についても考察する.

著者

香西 省治 角谷 良彦 西田 知博 植原 啓介 萩谷 昌己 萩原 兼一

雑誌

研究報告コンピュータと教育(CE) (ISSN:21888930)

巻号頁・発行日

vol.2020-CE-153, no.24, pp.1-10, 2020-02-08

---

文部科学省の大学入学者選抜改革推進委託事業(情報分野)で研究開発した CBT (Computer Based Testing) システムを実装面から概説する.本事業の目的は,思考力・判断力・表現力を評価する「情報科」の試験問題を研究することである.この評価のためには,紙による出題よりプログラミング能力などを効果的に評価しやすい CBT による出題の方が試験問題の幅を広げることができると考えた.この CBT システムは,「CBTならでは」の試験問題を受験者に出題することを重視して,実際に作成された「CBTならでは」の模擬試験問題を一般化・仕様化し,その後発生する仕様変更にも柔軟に対応できるブラウザ型の専用システムとして開発した.この CBT システムは,出題する試験問題を確認する作問機能部,受験者が受験するための機能を持つ試験機能部,試験結果を採点・集計する採点・集計機能部の 3 論理サブシステムから構成される.CBT システムによる試験実施運用シーケンスに基づく各論理サブシステムの動作と,プログラミング問題,ゲームブック型問題等の特徴的な 5 形態の試験問題の処理を示すことを通して,開発した CBT システムがこの事業で研究した「CBTならでは」の試験問題を出題できることを示す.尚,2017 年と 2018 年に実施した実証実験では,主にサーバ負荷の面で問題は発生していない.

著者

西田 知博 植原 啓介 角谷 良彦 鈴木 貢 中山 泰一 香西 省治 高橋 尚子 中西 通雄 松浦 敏雄 増澤 利光 萩谷 昌己 萩原 兼一

雑誌

情報教育シンポジウム論文集

巻号頁・発行日

vol.2017, no.28, pp.182-187, 2017-08-10

---

我々は,文部科学省委託事業 「情報学的アプローチによる 「情報科」 大学入学者選抜における評価手法の研究開発」 の中で,これまで情報入試研究会として実施してきた大学情報入試全国模擬試験を出発点とし,「思考力 ・ 判断力 ・ 表現力」 を評価するという視点も加えて 「情報科」 大学入学者選抜を CBT システム化するためにはどのような機能が必要かを検討している.ここではその検討経過と,今年度実施する試行試験用システムおよび,新しい出題フレームワークなど現在検討している出題方式を紹介する.